Coding into the Natural Numbers: The Very Idea

Posted in Logic, Semantics, Things that are true by nathanielforde

Have you ever been introduced to too many people at a party and come up with ad hoc nicknames, to keep track of who they were, how they knew the host etc? If so, congratulations you’ve successfully invented a coding schema.

Now imagine a party at Hilbert’s hotel with all its infinite guests. Suppose that each night they form a congo line alternating positions at random each night. It’s your task to keep track of the order of who follows who, but given that you can’t remember all their names you try to come up with a coding scheme which would uniquely identify each individual in the line… unfortunately the line is not finite, so you’ll need an infinite set of codes to describe the order of the line:

It’s at this point you might think of trying to number them. Only a moment later you realise how convenient this procedure is; after all an infinite of people can be labeled by an infinity of numerals! Call a congo line a sequence $<a_{0}, a_{1} .... a_{n} >$ where each of the dancers $a_{i}$ are currently nameless, and unknown to you.

We will consider a coding technique invented by Godel. The approach uses the fact that there are an infinity of primes to name the infinity of congo dancers. So for example we might specify the first dancer $a_{1} = p_{1}^{a_{1}+1}$ using the fact of the uniqueness of prime factorization to ensure that this label is unique. The “+1” is crucial for ensuring that we always have a positive exponent. So using this technique to we could define a concatenation operation on a congo line as the product of their unique labels:

$<a_{1}*a_{2}, ... *a_{n} > = \Pi_{i \leq n} p_{i}^{a_{i}+1}$

In this instance we characterize each line as the product of the labels of the dancers. We let the empty sequence

$<> = 1$
$<a_{1}*a_{2}> = 2^{a_{1}+1} \cdot 3^{a_{2}+1}$
$<a_{1}*a_{2}*a_{3}> = 2^{a_{1}+1} \cdot 3^{a_{2}+1} \cdot 5^{a_{3}+1}$
etc, etc…

But this doesn’t make much sense; how can we add or multiply dancers? Not obviously. However we could begin by categorizing types of dancers as graceful, quick, sultry, smooth, etc, then we can assign each type a distinct number, so the coding maps each type into a region of primes determined by the type of dancers in the sequence, thereby allowing us to represent each congo line as a chain of prime numbers with each member “scored” according to their type. Allow that we have a (in)finite alphabet of types, we say the types are coded as follow

# $a_{i} := 2$
# $b_{i} := 3$
# $c_{i} : = 6$
… associated with as many code numbers as required.

Now that we have named the parts, we might want to name the whole line. So we need to find a unique label for any sequence of dancers. We achieve this by multiplying the primes to determine a unique number for a sequence of any length, since each dancer has unique label each product will be unique. Hence, any numeral names a unique object, whether it be a sequence of dancers or a lonely dancer. So we can see that

# $< a_{1}, b_{2} > = 2^{a_{1}+1} \cdot 3^{b_{2}+1} = 2^{2+1} \cdot 3^{3+1} = 2^{3} \cdot 3^{4} = 8 \cdot 81 = 648.$

More succinctly, we could say:

# $<a_{1}* b_{2} > = 648.$

We need to do a little more work to show that this labeling system will allow us to recover the structure of each congo line by decoding. But of course all we need to do here is perform a prime factorisation, from which it is straightforward to recover that $648 = 2^{3} \cdot 3^{4}$ , from which we can unpack by definition our initial sequence as desired. This same pattern holds for more complicated congo lines.

Talking about dancing

We can now define several functions which will help us talk about dancing. Firstly we describe our congo line as a sequence, as only lines with this property are encoded by the prime-coding technique we used above. The following definitions apply to sequence numbers only. But they’re pretty straightforward. You might want to describe the length of a congo line, or recover the participants from the #name we have given the line, and we can do this with the following function. Let $a := <a_{1}*a_{2} .... *a_{n} >$ , and define

$Seq(a) := \forall p, q \leq a (Prime(p) \wedge Prime(q) \wedge q< p \wedge p | a \rightarrow q|a) \wedge a \neq 0.$ [Sequence Number]

$lth(a) := \mu k \leq a+1 ( \neg (p_{k} | a))$ [Length]

$(a)_{i} := \mu k \leq a$ $( (p_{i}^{k} | a \wedge \neg (p_{i}^{k+1} | a) \dot{-}1).$ [Decoding]

So let’s see how the length of a string can be recovered. From any number #(a) we have its prime factorisation, so the trick to decomposing each element in the factorisation, for instance take $lth(12)$ and we find that $p_{3} = 5 \wedge \neg(5 | 12)$ and then we see that $lth(12) = lth(<2^{2} \cdot 3>) = 3.$ In general $lth(a) = n+1$ where $a = <a_{1} .... a_{n}>$ because $<> = 1$ by definition.

Similarly, we check $(12)_{1}$ by finding that $p_{1} = 2$ , and $p_{1}^{2} = 4$ which divides 12 but we also have $p_{1}^{3} = 8$ does not divide 12 as desired. So we have $k = 2$ which is positive as desired. Next we test $(12)_{2}$ by observing $p_{2} = 3$ and choosing $p_{2}^{1} = 3$ so choose k = 1, so that we have 3 divides 12, but 9 does not. Furthermore 3 is positive, so we can conclude that the 12 decodes into its unique prime factorisation $2^{2} \cdot 3$ . Here we knew in advance the correct decoding, but in general we test the appropriateness of a decoding procedure by multiplying each sequentially discovered component until such time as the product reaches (or exceeds) the coded number, $(12)$ in our case.

Talking about anything else.

So far we have suggested that we could use this coding technique to simplify discussions about congo lines, but this is merely one application. In fact the prime-coding technique is versatile enough to encode any structure. In particular we shall come to see how it can effectively encode sentences of the rich logical language $\mathbb{L}$ and the sequential action of Turing machines. The same fundamental idea underlies both approaches, we wish to be able to take any string of sentences $< \phi_{1}, .... \phi_{n} >$ , or action sequence $< a_{1}, .... a_{n} >$ and code them in the natural numbers, so that we may give each sequence a name. We adopt the following notation:

$\ulcorner n_{i} \urcorner \text{ is the godel number of } \phi_{i}$

This utility allows us to express claims about the object $\ulcorner n_{i} \urcorner$ in our language $\mathbb{L}$ . So if $\mathbb{L}$ is a rich first order language capable of speaking about numbers, we can treat $\ulcorner n_{i} \urcorner$ as first order object and make expressive claims about the properties of the object in question. This is a key point, your language must be sufficiently expressive to talk about numbers in the first place, if we are going to use numbers as a code for other objects! In our case the object is the sentence $\phi_{i}$ , so defining a predicate: $N(x) := \{ x | x \text{ are nice sentences } \}$ we can claim $N(\ulcorner n_{i} \urcorner )$ and expect to be able to evaluate such a claim according to the semantics of $\mathbb{L}.$

The generality of this technique is truly staggering once you perceive it. Any language, or system capable of identifying the natural numbers can use the prime coding technique to code its own expressions is then capable of expressing claims about its own syntax. Allowing the expression of a “meta-level” reflection about the properties of any constructions developed within our own language. Constructions such as novels, poems and proofs – some of which are certainly nice.

This expressivity allows for Godel’s famous incompleteness result; about which, more later.

23Feb2014

Intuitive Algorithms and Primitive Recursion

Posted in Logic, Philosophy, Semantics, Things that are true by nathanielforde

In the last post here we examined the strategy of the Squeezing argument. In this post we’ll try to apply this strategy to the notion of an intuitive algorithm or calculable function. We’ll begin with an attempt to gloss the notion of an intuitively calculable function. The gloss:

The notion of an intuitive algorithm is often specified by example. Rogers suggest a few candidates as follows:

The Euclidean Algorithm for finding greatest common divisors,
Eratosthenes’ Sieve for finding prime numbers
Addition and multiplication

The second way in which the notion of an algorithm can be clarified is a generically as a step-wise procedure for determining the answer to some specific question. Naturally, there are some restraints on the notion of a step-wise procedure; you might want to insist that the algorithm has to be completed in a finite series of steps. In other words we must be able to perform the procedure within a finite span, given finite resources of memory and enthusiasm.

Let’s make a small idealisation here, take every question to indicate a specific problem with a number of parameters. Given our specification that we ought to be able to answer this question we must be able to review each parameter in a finite amount of time. So we might want to insist that no question can ask too much of us, hence each question should admit comprehension by a finite mind.

This can be made precise:

We take a problem to be a question (perhaps a coded question) on the natural numbers. What is the result of $f(x_{0} ... x_{n})?$ The answer is calculable if the value of $f(x_{0}....x_{n})$ can be found in finitely many steps. An intuitively calculable function is a method applied to address a problem within a finite series of steps.

Every intuitive algorithm is an answer to an effectively calculable problem. This is not to say there is an efficient calculation, just that there is an effective method (algorithm) which ensures an answer.

Call a problem computable if it can be answered by a computer. Now consider what kinds of questions can computers answer – can each problem be resolved by a computer? A famous thesis in computer science answers this positively, but no proof exists.

The Church Turing Thesis: Every effectively calculable problem is a computable problem.

This thesis is stated to be unprovable because the class of effectively calculable problems cannot be identified a priori, or at least that’s the common wisdom. Hence, they can’t (it’s argued) be identified with the class of computable problems which can be well defined.

At this stage I’ve thrown allot of labels at you. There are two crucial points to take away (i) the intuitive (undefined) notion of an algorithm underwrites the notion of effective calculability, and (ii) the computable functions, in contrast, are well defined.

What is a Computable Problem?

Historically, this question has found three answers. Mathematically each answer can be seen to be equivalent. We will discuss two, so as not to overly clutter the page with redundancies.

On the one hand we have a characterisation of how a computer works by means of recursive functions. On this view a computable problem is seen as a question about the value of a function $f(x_{1} .... x_{n})$ if there is a procedure for determining the value. Specifically, a procedure enacted by the performance of a sequence of the primitive recursive functions, each of which is free (if need be) to effect an unbounded search of the function space. The idea, perhaps unsurprisingly, is that the set of recursive functions is defined recursively from all the logically possible combinations of a small collection of primitive functions. More precisely:

We say the following initial functions are primitive recursive:

$Z(x) = 0$
$S(x) = x+1$
$p_{i}^{k}(x_{1}, x_{2}, ... x_{k}) = x_{i}$

The first being the zero function, the second being the successor function and the third is a class of projection functions defined $\forall i, k$ such that $i \leq k$ . Think of these as selective maps between a set of inputs and a particular output.

We also note that a set of functions are closed under composition, for if $\{ g, f \}$ are functions, then [; f(g) = h ;] is a function. The primitive functions are those created by applications of composition on the initial functions.

Furthermore, we note that a set of functions is said to be closed under primitive recursion, if the recursion equations

$f(0, x_{2} .... x_{k}) = h(x_{2} ....x_{k})$

$f(x_{1}+1, x_{2} ... x_{k}) = g(x_{1} .... x_{k}, f(x_{1} ... x_{k})).$

hold. In the jargon of computer science we say that a recursive function is one which calls itself in its own definition, i.e. it is defined in stages successively by iterating on the values achieved at earlier stages. The class of primitive recursive functions is the smallest set S, which contains the initial functions and is closed under primitive recursion and function composition.

This may not seem like much but these structures are at the root of every programming language ever created. To give a flavour of their adaptablilty we will show how to use these functions to define, addition, multiplication and exponentiation. With these notions defined it is easy to see that all polynomial functions are primitive recursive. Hence, all polynomial problems are computable. This result should go some distance toward convincing you that a recursive (read computable) problem is an effectively calculable problem.

Addition

We show that the addition can be defined by recursion. Define $a(x, y) = x + y$ then we can pick a function $h(y) = p_{1}^{1}(y) = y$ and another function $g(x, y, z) = S(p_{3}^{3}(x, y, z)) = S(z).$ Now we define as follows:

$a(0, y) = h(y) = y \\ a(x+1, y) = g(x, y, a(x, y)) = S(a(x, y)) = a(x, y)+1$

This is well defined since it can shown to be a function resulting from the composition of initial function, under primitive recursion. Better, the definition captures our intuitive algorithmic procedures; take $a(1, 2) = S(a(0, 2)) = 2+1 = 3$ . Hopefully, you agree this is correct, if not you should probably stop reading.

Multiplication

Now we can see that the multiplication function can also be defined. Let $m(x, y) = x \times y$ and take the following functions $h(y) = Z(y)$ , $g(x, y, z) = a(y, z)$ , then we can note that:

$m(0, y) = h(y) = 0 \\ m(x+1, y) = g(x, y, m(x, y)) = a(y, m(x, y)) = y+m(x, y)$

This also captures our expectations of the intuitive multiplication algorithm. By example, take $m(2, 2) = g(1, 2, m(1, 2)) = a(2, m(1, 2)) = 2+ 2 \times 1 = 2+2 = 4.$ The idea should be becoming clear by now. The sequential operation of the recursive formulation allows us to establish a well defined composition operation iteratively as we ascend through the natural numbers.

Polynomial Functions

Now since we can define exponentiation as as iterations of multiplication we can conclude that any polynomial $p(x)$ having natural numbers as coefficients is primitive recursive. Any such function $p(x)$ is primitive recursive. This result covers a wide range of functions, and you might be inclined to think all calculable problems can be seen as result from sequential applications of primitive recursion, as indeed many more are. However, we can show that there exists functions not calculable by means of primitive recursion. We shall show here, that the Ackermann function is not primitive recursive but it is recursive. The distinction is crucial.

What is a Recursive Function?

The set of recursive functions is the set of primitive recursive functions which are also closed under the operation of unbounded search. We say that a function $g$ performs an unbounded search on the variable $x$ , just in case for all $\overrightarrow{y_{n}}$ the following holds:

Unbounded Search for $g$ :

$f(\overrightarrow{y_{n}}) =$ $min \{ x | g(x, \overrightarrow{y_{n}}) = 0 \wedge \forall(z)_{< x} g(z, \overrightarrow{y_{n}}) \downarrow \}$ $\text{ if the minimum exists; undefined otherwise. }$

In words, we have stated that there is a function $f(\overrightarrow{y_{n}})$ which performs a search to find the minimal free element which satisfies the function $g(x, \overrightarrow{y_{n}}) = 0$ , where the function is also defined for values less than $x$ . More often we will write this as an instance of $\mu$ -recursion: $\mu x [G(x, y_{1} ... y_{n})]$ With this addition we have may step through the natural numbers until we find an appropriate sequence which satisfies our condition. So for any condition which we could define on the primitive recursive functions, we can effect a search of the function space to determine which, (if any) is the minimal point at which our condition is satisfied. This doesn’t change the general observation that primitive recursive procedures surely map to effectively calculable problems, it only adds flexibility to how we apply our recursive procedures since we can now specify algorithmic operations to kick into effect at selective stages in our function space.

Are Recursive procedures Effectively Calculable?

The answer is an obvious yes since each of the procedures, of search, composition and function application are capable of being performed by a finite human mind. So we have set up the first premise of our Squeezing argument. From this the easy direction follows, and we can see that:

If the function $\phi$ is recursive then $\phi$ represents an effectively calculable method on our problem space.

It remains to show the more controversial premise of the squeezing argument, by proving that (i) there is a characterisation of computation (namely modified Turing Machines) equivalent to the recursive characterisation such that (ii) any effectively calculable method of problem solving finds an equivalent method in the Turing Machine model of computation. Using these two facts we can establish that the Church Turing Thesis is valid, if you buy the Squeezing argument. We shall assess the potential for establishing these claims in the next post.

15Feb2014

The Squeezing Theorem and Exactitude

Posted in Logic, Philosophy, Semantics, Things that might be true by nathanielforde

“Clowns to the left of me, jokers to the right…It’s so hard to keep a smile from my face.”

In this post we will (a) prove the squeezing theorem about the limits of functions, and (b) then examine Kriesel’s Squeezing argument for the intuitive notion of logical validity. The goal will be assess the manner in which such arguments lend exactitude to imprecise intuitions. The hope is that using a squeezing argument we may be able to provide a general method for making a vague notion mathematically concrete. We will show the whole issue turns on what counts as “vague”.

The Squeezing Theorem:

We wish to prove, that if

$[; \lim_{x \to x_{0}} f(x) = A \wedge \lim_{x \to x_{0}} g(x) = A ;]$

and we have

$[; f(x) \leq h(x) \leq g(x) \text{ for all x in the interval I } ;]$

then we have it that

$[; \lim_{x \to x_{0}} h(x) = A ;]$

This theorem can be best be envisioned by thinking of two policemen escorting a rowdy prisoner into a jail cell. No matter how wildly the prisoner bucks, if the two policemen end up in the jail cell so too will the prisoner they’ve escorted there. In other words, no matter how unpredictable the movement of $[; h(x) ;]$ , we may chart the trajectory of the function if it’s action can be constrained the operations of two other functions $[; f, g ;]$ .

This theorem makes a vague function more precise and mathematically tractable. We now prove it to be valid.

The Proof

From our our first assumption we know that

$[; \exists \delta_{1} \delta_{2} \text{ s.t. } | f(x) - A | < \epsilon_{1} \wedge |g(x) - A | < \epsilon_{2} \text{ whenever } 0 < |x - x_{0}| < \delta_{i} ;]$

Consider that we also so know that any value of $[; h(x) ;]$ falls between the values of $[; f, g ;]$ . So we may attempt to prove that $[; \forall \epsilon (\epsilon > 0) ;]$ we can find a $[; \delta ;]$ such that

$[; |h(x) - A| < \epsilon \text{ whenever } 0 < |x - x_{0}| < \delta ;]$

But since $[; f(x) \leq h(x) \leq g(x) ;]$ it follows that:

$[; |f(x) - A| \leq |h(x) - A| \leq |g(x) - A| ;]$ .

Let $[; \delta = max\{ \delta_{1}, \delta_{2} \} ;]$ . Now pick any distance measure [; \epsilon ;] and we can see that

$[; -\epsilon < |f(x) - A | \leq |h(x) - A| \leq |g(x) - A| < \epsilon ;]$

because we know from our first assumption that $[; |f(x) - A| \text{ and } |g(x) - A| ;]$ fall within any [; \epsilon ;]-measure whatsoever. So it follows directly by the transitive property of inequality that:

$[; - \epsilon < |h(x) - A | < \epsilon ;]$

as desired. So we have can conclude

$[; \lim_{x \to x_{0}} h(x) = A ;]$ .

The Squeezing Argument

The proof we just performed demonstrates a method by which we can observe an increased exactitude in our assessment of a previously unknown parameter. The question remains; can we use such a method outside of mathematics to minimize imprecision in other domains? Consider an argument from Kriesel to the effect that the “intuitive notion of validity” is appropriately isolated as a property of all and only those arguments which are provably valid within a proof system, that may (in turn) be modeled in a Tarski style truth functional semantics. The idea is that we can use these two formal notions of syntactic and semantic validity to sandwich the intuitive notion of intuitively valid inference. So like the drunk between two policemen, all those conclusions arrived at by our “formal” notions of valid inference ought to be held as valid intuitively too.

The argument proceeds as follows: Take your intuitive notion of valid inference, imagine your favorite instances of a valid arguments and note that they seem to be true in virtue of their form alone e.g [; (\phi \rightarrow \psi), \phi \vdash \psi ;]. That is to say that no matter the nature of the premises, if we substitute them uniformly into positions in our favorite argument, then we will have a new valid argument.

We’ve cheated here a little bit by representing your favorite argument (Modus Ponens) schematically in the notation for propositional logic. But this move is tolerable in that it points to an intuitive notion of “valid in virtue of form” without strictly defining it. We could also simply have said that:

[; \text{ If } \psi \text{ follows from } \phi \text { and } \phi \text{ is true, then } \psi \text{ is true too whatever the values of our propositions } ;]

We claim that [; \psi ;] is validly concluded from our premises simply by the form of the argument. The notion is deliberately somewhat vague, since we’ve have made no effort to clarify validity or form…but the squeezing argument aims to show that we don’t need a more exact clarification because we can find equivalent notions of validity which circumscribe what it would mean to say that an argument is “valid in virtue of form.”

Syntactic Pressure

On the one hand we find the standard proof theoretic notion of validity, where an argument is conducted in, for instance, a natural deduction system which has very precise rules on what counts as a valid conclusion from any set of premises whatsoever. These rules govern the syntactic manipulation of the sentences in a formal language [; \mathbb{L} ;]. For instance reasoning from conjunctive claims has very precise behavior determined by two syntactic rules:

[; \dfrac{\phi_{1} \& \phi_{2}}{\phi_{i}} \& E \text{ and } \dfrac{\phi_{1}, \phi_{2}}{\phi_{1} \& \phi_{2}} \& I ;]

These rules are called introduction and elimination rules the conjunction operator. Similarly, we have rules governing conditional reasoning:

[; \dfrac{(\phi \rightarrow \psi), \phi }{\psi} \rightarrow E \text{ and } \dfrac{ | \phi | …… \psi}{ \phi \rightarrow \psi} \rightarrow I ;]

The behavior of [; \& ;] shouldn’t need any explanation, and [; \rightarrow E ;] is just modus ponens, but [; \rightarrow I ;] is more interesting. This rule states that if we assume [; \phi ;] and in the course of syntactically manipulating our premises we arrive at [; \psi ;] we may conclude [; \phi \rightarrow \psi ;]. Putting this together we can construct the following argument.

[; | \phi \& \psi | ;] Assumption
[; \phi ;] by &E, (1)
[; \psi ;] by &E, (1)
[; \psi \& \phi ;] by &I, (2), (3)
[; (\phi \& \psi) \rightarrow (\psi \& \phi) ;] by →I (1), (4).

This argument proves that conjunction is order invariant with intuitively acceptable rules of premise manipulation. As such, we wish to say that the argument is also valid in virtue of form, since regardless of the nature of our premises the syntactic rules would apply. It is our acceptance of these arguments that allow us to construct the soundness proof for classical logic. The proof is by induction on the length of any argument constructed in the classical system. For an argument of any length each step proceeds by an application of an intuitively acceptable rule, so if the argument is syntactically correct we must accept the conclusion of the argument as intuitively sound too since we can’t fault any step in the reasoning. On this basis Kriesel asks us to accept the claim that:

If [; X \vdash_{nd} \phi ;] then [; \phi ;] follows in virtue of form from the premises X.

In words, the claim states that if the conclusion is a valid consequence of the premises X in our natural deduction system then we may also say that the conclusion is intuitively valid too.

Semantic Pressure

From the other direction we build models and specify precise criteria for when a claim is true on a model. Again we take the formal language [; \matthbb{L} ;] and specify rules for evaluating claims constructed in the language. So on a model [; M ;] we would say that [; M \models \phi ;] holds whenever the state of affairs [; ||\phi || ;] exists in the model. So if [; \phi ;] describes the angle of a building in our model, then [; \phi ;] is said to be true just when the building is angled as described. False otherwise. We build up the semantic definition to incorporate the syntax of [; \mathbb{L} ;]. In particular we have:

[; M \models \phi \& \psi \Leftrightarrow || \phi || \in M \text{ and } || \psi || \in M ;]
[; M \models \phi \rightarrow \psi \Leftrightarrow || \phi || \not\in M \text{ or } || \psi || \in M ;]

On this understanding we can construct and evaluate arguments as valid only when their is no interpretation of the model that could make the premises true and the consequence false. Intuitively this means, an argument is valid just when there is no way of evaluating the premises and falsifying the conclusion. So whether [; \phi \& \psi ;] is true or false in the model, if we assume it’s true we ought to be able ensure the [; \psi \& \phi ;] is true too. More particularly we must be able to conclude that [; M \models \phi \& \psi \rightarrow \psi \& \phi ;] . If the antecedent is true in the model this is obvious from the semantic definition of [; \& ;], but if the antecedent is false, the claim is vacuously true and holds. So for whatever the evaluation of the particulars the argument holds, and hence the semantics of [; \& ;] is order invariant.

Now since an argument with true premises and a false conclusion can’t be valid, never mind valid in virtue of the form, we can see that:

[; \text{ If } M \nvDash \phi \text{ then } \phi \text{ does not follow validly in virtue of form from any premise set describing } M ;]

By the contraposition of this claim it follows that any argument valid in virtue of form derived from the premises describing M will be semantically valid in the model M.

Tidying Up

So we have already observed that the set of syntactically valid conclusions are all intuitively valid in virtue of their form, and we have just seen that any intuitively valid argument can be modeled semantically. More visually we have the following situation

[; Syn = \{ X, \phi | X \vdash_{nd} \phi \} \subseteq Int = \{ X, \phi | \phi \text{ intuitively follows from } X \} \\ \subseteq Sem = \{X, \phi | X \vDash \phi \} ;]

But by the completeness theorem for classical logic we know that [; Syn = Sem ;]. So we now know that

[; Syn = Int = Sem ;]

which ensures that the vague intuitive notion of “valid in virtue of form” is coextensive with two mathematically precise notions of validity.

The Crucial Step

The use of the soundness proof is a good motivation for this argument as syntactic validity lends some substance to the informal notion of formal validity. But we can imagine a case where a non-classical logician could argue similarly so long as they can prove a soundness result on some non-classical model. However, the non-classical logician will still need to avail of a meta-level conditional operator which preserves the validity of contraposition if they are to argue as above that semantic validity also constrains intuitive validity. It would be strange, but possible to argue that the intuitive notion of validity was coextensive with a definition of logical validity that did not preserve contraposition, while informally availing of it.

This hints at the idea that “intuitive validity” can be squeezed between a number of different consequence relations, and the manner in which we squeeze depends wholly on how we specify the meanings of the logical connectives (i.e &, →, etc ) governing those relations. Either syntactically or semantically there are a number of candidate options such as intuitionistic and relevantist logics. None is obviously more accurate as a representation of the colloquial notion of validity, so the degree to which a Squeezing argument is strictly and mathematically compelling depends on how appealing you find the characterization of soundness. For better or for worse our estimation of whether an inference is sound seems to depend to a degree on the context in which the inference is made. In this manner our intuitive notion of validity should be expected to fluctuate. However, the squeezing argument ensures that notion of contextual validity can be made precise with a little patience.

Can we make a general class of Squeezing theorems?

Peter Smith argues in favor of this notion so long as the first step on the route to generating a Squeeze theorem renders the “vague” candidate clear in some specific sense. So the notion of computability, like the notion of validity has an intuitive reading which can be made slightly more precise by an appeal to specific examples or a generic gloss. The use of these examples allows us to find general formal notions of computability, validity which capture the paradigm examples. In this manner we move along a trajectory of conceptual sophistication aiming for an increased exactitude. In the next few posts we’ll assess Smith’s argument to effect that Squeezing arguments can be used to establish a proof of the Church-Turing thesis.

Aspiring PI

"An orgy of abstract informality" – reader review

Category Archives: Semantics