Tag: Tarski

Atomless: The Calculus of Systems of (Almost) Any Logic 

Bas van FraassenLeave a comment

A logic L is a closure operator on a set of sentences S (of a syntax SYNT). An L-theory is a subset of S closed under L, and an L-theorem is a sentence that belongs to all L-theories.  (A logic may not have any theorems.)  A sentence A is an L-consequence of set of sentences X exactly if A is in L(X).

The L-theories, being the L-closed sets, form a complete lattice CL, which Tarski called the calculus of systems of that logic.  This lattice is bounded above and below, respectively by S and L(Λ), the L-closure of the empty set.  The latter contains only the set of theorems of L, if any, and is therefore also said to be trivial.  

In a lattice, an atom is an element that is not the bottom but has no element between it and the bottom.  Precisely:

Definition.  An L-theory X is an atom of the calculus of systems of L if and only if X is not trivial but has no non-trivial proper sub-theory.

So far, so general.  I wish to remark that in almost all cases, and certainly for all familiar logics, this lattice is not atomic, in fact has no atoms at all.

Definition.  Logic L is disjunction minimal exactly if:

  1. S is a set of finite strings generated from an infinite set of propositional variables
  2. The syntax SYNT includes a binary connective v such that
    1. if A, B are sentences then A v B is an L-consequence of A
    1. if A is not an L-theorem, and q is a propositional variable that does not occur in A, then A v q is not an L-theorem, and A is not an L-consequence of A v q.

Result.   If logic L is at least  disjunction minimal then its calculus of systems CL has no atoms.

Argument.

Suppose X is a non-trivial L-theory, and A is a member of X that is not an L-theorem.  Since A is finite there is a propositional variable q which does not occur in A.  Then A v q is a member of X, and is not an L-theorem, and A is not an L-consequence of A v q.

Therefore L({A v q}) is a non-trivial proper sub-theory of X, for it is part of X, includes A v q which is not an L-theorem, and it does not include member A of X.  Hence X has a proper non-trivial sub-theory.

So, if L is at least disjunction minimal, and X is any non-trivial L-theory, then X is not an atom of calculus CL. Hence CL has no atoms.

Remark. Almost all, but not all logics in the literature are at least disjunction minimal. An exception is the Weak Kleene logic WK3 where A does not entail A v B. See Jc Beall (2016) “Off-Topic: a new interpretation of Weak Kleene logic”. Australasian Journal of Logic (13: 6), Article 1.

On Tarski’s Calculus of Systems (2)

Bas van FraassenLeave a comment

The relation between negation and infinity loomed large in the Intuitionist critique of mathematics.  But when we come to Intuitionistic logic, it turns out to be all about the conditional.  Negation comes in just by means of a definition:  ~A =def A → f.  

It is in the logic’s realizations that the intimate relation between negation and infinity comes to the fore.  Recall from the previous post that the lattice of theories of any distributive logic is a complete Heyting lattice with zero element Cn(𝜙), and

T → T’ is the weakest (largest) theory X such that T ∩ X ⊆ T’; 

T → T’ = ⊕{T’’: T ∩ T’’ ⊆  T’)

The pseudo-complement ¬T of T, if it exist, must be the weakest element X which is contrary to T, that is, it is such that T ∩ X ⊆ Cn(𝜙).  So we instantiate the above:  ¬ T is the weakest element X such that  T ∩ X ⊆  Cn(𝜙)), hence:

¬ T  = T → Cn(𝜙).  Equivalently, ¬ T = ⊕{T’: T ∩ T’ ⊆  Cn(𝜙)}. 

So much, so general.  How does it happen that the Laws of Excluded Middle and of Double Negation fail in Intuitionistic logic, and their corresponding principles fail in the calculus of systems?

To continue, let L be classical propositional logic, with & and ~ as primitive connectives and let S be the set of all sentences.  Thus S = Cn(S) is the unit (top) of the lattice. For brevity, if A is a sentence I will write  “Cn(A)” for “Cn({A})”.

Note: Contrariety, the condition T ∩ T’ ⊆  Cn(𝜙), is different from mutually inconsistency.  With p, q atomic sentences, Cn(𝜙) is contrary to but consistent with Cn(p), Cn(p) and Cn(~p) are both mutually inconsistent and contrary. But Cn(p & q) and Cn(~p & q) are mutually inconsistent, their join is S, but not contrary for their intersection contains non-theorem q.  Contrariety is this:

Theorem 1.  T ∩ T’ ⊆  Cn(𝜙) iff for every non-theorem A in T there is a consistent extension of T’ that includes ~A.

To prove this we can appeal to the general features of theories in classical logic:

  • any consistent theory is part of a maximal consistent theory 
  • every theory is the intersection of all its maximal consistent extensions
  • for all sentences A, if T is a maximal consistent theory then T contains either A or ~A 
  • if T does not imply A then T has a maximal consistent extension that includes ~A 

Proof.  

  •  Let A be any L-non-theorem in T.   Suppose that T’ has no consistent extension that includes ~A.  Then A is in all the maximal consistent extensions of T’, hence in T’, hence in T ∩ T’,  which is thererfore not included in Cn(𝜙).
  •  Suppose that for every L-non-theorem A in T, T’ has a consistent extension which includes ~A.  Then if A is an L-non-theorem in T, A is not in T’, and hence not in T ∩ T’.  If A is an L-non-theorem that is not in T then it is also not in T ∩ T’.  Therefore T ∩ T’ contains only L-theorems, and is Cn(𝜙).

Lemma 1. Cn(~A) ⊆ ¬Cn(A)

If E is in Cn(A) there is a sentence B such that E is equivalent to A v B.  For each such sentence Cn(~A) has a consistent extension that includes ~(A v B).

  • If ~A entails B then it too entails A v B, so then A v ~A entails A v B, hence A v B is an L-theorem.
  • If ~A does not entail B then Cn(~A) has a maximal consistent extension that includes ~B, which includes ~A & ~B.

So by Theorem 1, Cn(A) ∩ Cn(~A) ⊆ Cn(𝜙). Hence Cn(~A) ⊆ CnA) → Cn(𝜙) = ¬Cn(A).

Theorem 2.  If T is finitely axiomatizable then T Θ ¬T = S

Because of the classical conjunction rules, if T is finitely axiomatizable then there is a sentence A such that T = Cn(A).  By the lemma, Cn(A) Θ  Cn(~A) ⊆ Cn(A) Θ  ¬Cn(A).  But Cn(A) Θ  Cn(~A) = Cn(Cn(A) ∪  Cn(~A)) = S.

It follows then that violations of Excluded Middle can only be by theories that are not finitely axiomatizable.

To pursue this we need to improve on the above lemma.

Lemma 2.   T ∩ T’ ⊆  Cn(𝜙) iff for every non-theorem A in T there is a maximal consistent extension of T’ that includes ~A.

This follows at once from Theorem 1.

Lemma 3.  If T ∩ T’ ⊆  Cn(𝜙) then T’ ⊆ ∩ Cn({~A: A is in T})

Suppose T ∩ T’ ⊆  Cn(𝜙) and that A is an L-non-theorem of T.  Let KT’(A) be the set of all consistent extensions of T’ that include ~A.  So ∩KT’(A) ⊆ Cn(~A). Let MT’ be the set of all maximal consistent extensions of T.  Then for each L-non-theorem A of T:

            T’ = ∩MT’ ⊆ ∩KT’(A) ⊆ Cn(~A). 

Since T’ has a consistent extension that includes ~A for each L-non-theorem in T it follows that T’ ⊆ ∩{Cn(~A): A is an L-non-theorem in T}.  From this the lemma follows because if A is an L-theorem then Cn({~A}) = S, which has no effect on the intersection.

Theorem 3.    ¬T = ∩({Cn{~A}: A in T}).

First, it is clear that for every L-non-theorem A in T, ∩({Cn{~A}: A in T}) has a consistent extension that includes ~A.  Therefore ∩({Cn{~A}: A in T})  ⊆  ¬T by theorem 1 and definition.  

Secondly,  T ∩ ¬T ⊆  Cn(𝜙), so by Lemma 3, ¬T ⊆ ∩ Cn({~A: A is in T})

Corollaries:  Cn({~A}) = ¬Cn(A), ¬Cn(𝜙) = S, ¬S = Cn(𝜙)

This theorem gives us a way to identify the pseudo-complement of theories that are not finitely axiomatizable.

Example. Let AT be the infinite list of atomic sentences p1, …, pm , … and T = Cn(AT).  Let ATfin be the set of finite conjunctions of atomic sentences. Every member of T is equivalent to a finite conjunction C of atomic sentences disjoined with some other sentence A (e.g. p v q).  

So ¬T = ∩ Cn({~(C v A): C in ATfin})

As an example, consider the L-non-theorem (p1 & ~p2). Could it belong to ¬T?  It does not belong either to Cn(~p1) or to Cn(~p2). Nor does it belong to Cn(~q) for any q in ATfin other than  p1 or p2.

We can generalize this reasoning to cover any L-non-theorem.  Since L is classical propositional logic, we can think in terms of truth-table rows or their generalization: 

a finite state-description is a consistent conjunction p*1 & …& p*m of  atomic sentences each of which either has or does not have an appended negation sign. 

In classical propositional logic,  A is an L-non-theorem if and only if there is a finite state-description B such that B├L~A.  For any such B, since B is finite and AT is infinite, there is an atomic sentence q which does not appear in B.  But then B is not in Cn(~q), hence not in ¬T.  Therefore there is no derivation of ~A in ¬T.  Hence ¬T = Cn(𝜙).

This gives us a counterexample to both Excluded Middle and Double Negation, with T = Cn(AT):

            T ⊕ ¬T = T and T ≠ S

            ¬ ¬T = ¬ Cn(𝜙) = S and S ≠ T

The following analogy strikes me as apt.  Remember that ¬T  is also the join of its contraries.  There are uncountably many infinite state descriptions, all inconsistent with each other.  So we can look to continua for analogies. In a geometric space, the join of a family of subspaces is the least subspace that contains all.  Suppose P is a plane, its subspaces are the straight lines through the origin.  Take away one such straight line:  the join of the remaining ones is still the entire plane.

On Tarski’s Calculus of Systems(1)

Bas van Fraassen2 Comments

Tarski’s calculus of systems is what we would now call the lattice  of theories in classical propositional logic.

For this lattice Tarski made an interesting claim, about its relation to Intuitionistic logic.  In effect, he asserts that it is a Heyting algebra:

“we might say that the formal relation of the calculus of systems to the ordinary calculus of classes is exactly the same as the relation of Heyting’s sentential calculus to the ordinary sentential calculus.” (Tarski 1935: 352)[i]

The concepts he introduced were very general. My aims here are two. First, to outline these ideas in a general form, independently of classical logic. Second, to explain to myself exactly why his claim, about that relation between classical and Intuitionist logic, is correct. 

Intuitionistic logic

This logic can be presented in many ways, but here is my favorite.  The sentential syntax has primitive binary connectors &, v, →, and the propositional constant f, the falsum.  For &, v, and f the rules are the same as in classical logic.  In addition Intuitionistic logic has the Great Law of Implication:

            A, B├ C if and only if A├ B → C

That is all, except for an important definition

            ~A =def A → f

Modus Ponens is valid, so is Distribution.  But Excluded Middle, Double Negation, and ‘bad’ Reductio (~-elimination) fail.

It is my favorite for it connects almost word for word with the algebraic version:

Definition.  A Heyting (aka Brouwerian) algebra is a lattice L with zero element and an operation → such that for all x, y, z in L, x ∧ y ≤  z if and only if x ≤ y →  z.

A few terms

The terms I use will mostly not be Tarski’s.  In my terminology a logic is a consequence relation L, of some sort, on a given set of sentences S.  The theorems of logic L are the sentences that are the L-consequences of the empty set 𝜙.  A derivation of sentence A from set of sentences X in L is a finite sequence of sentences of which the last is A, and each of which either is a member of X or is an L-consequence of the preceding sentences in the sequence.  

Finally, sentence A is an L-consequence of X if and only if there is a derivation of A from X in L. So a logic is, at the least, a finitary consequence relation.  I will write X ⊢L A  for “A is an L-consequence of X” when convenient.

A theory of L (or, in L, or an L-theory) is a set of sentences that contains all its own L-consequences.  The operator

            Cn(X) =def {A: A is an L-consequence of X}

is thus a finitary closure operator on the set of sentences S,  and the L-theories are precisely the closed sets, i. e. sets X such that X = Cn(X). 

It is a general theorem (Birkhoff 1947: 112, Thm.2 Corollary) that the closed sets of a closure operator form a complete lattice pre-ordered by set inclusion with the closure of {𝜙} as zero element, and the operations ∩ as meet (inf) and ⊕ as join (sup), with the definition: 

Definition.  If T and T’ are L-theories, their join is T ⊕ T’= Cn(T ∪  T’).

The infinitary forms of those two operations are well-defined also, given that this is a complete lattice. For example, the principle that if T ⊆ T’’ and T’ ⊆ T’’ then T ⊕ T’ ⊆ T’’ generalizes to: if T ⊆ T’’ for all T in a set X of theories then ⊕X ⊆ T’’.

Distributive Logics

If L is a propositional logic pertaining to a sentential syntax with primitive connectives & and v, I will call L distributive iff for all sentences A, B, C:

            [1] A ⊢L A v B,           B ⊢L A v B,    If B ⊢L A,  and C ⊢L A then B v C ⊢L A

            [2] A, B ⊢L A & B,     A & B ⊢L A,   A & B ⊢L A

            [3] (A v B) & (C v D) ⊢L A v (B & C)

            [4] A & (B v C)  ⊢L  (A & B) v (A & C)

Clearly classical logic is distributive, but so are Intuitionistic logic and FDE and many others.

Lemma.  If L is a distributive logic, then: if B ⊢L A and C, D ⊢L A then B v C, B v D ⊢L A

For proof see Appendix.

Theories in distributive logics

From here on the target logic L of our discussion will be a distributive logic, and the calculus of systems will be the theory of theories in a distributive logic.

Not all complete lattices are completely distributive.  To be a complete Heyting lattice the following infinite distribution equality must hold:

            T ∩ ⊕{Ti} = ⊕{T ∩ Ti}

for arbitrary index set {i}(Birkhoff 1967: 128).  

That this holds in the calculus of systems follows from the fact that derivations are finitary, and the theories are theories of a distributive logic.

Suppose first A is in T ∩ ⊕{Ti}.  Then there is B in T such that there is a derivation of A from B.  In addition there are sentences A1, …, Am taken respectively from T1 , …,Tm, for some finite set of indices 1, …, m, from which there is a derivation of A.  The sentences B v A1, …, B v Am  belong to T and also to T1 , …,Tm respectively.  Hence they belong to  T ∩ Tj for j = 1, …, m respectively, and hence to ⊕{T ∩ Ti}.  

Recalling the Lemma for distributive logics, we conclude that there is a derivation of A from B v A1, …, B v Am, with all these sentences belonging to ⊕{T ∩ Ti}

Suppose second that A is in  ⊕{T ∩ Ti}.  Then there is a derivation of A from premises and A1, …, Am taken respectively from T ∩T1 , …,T ∩Tm, for some finite set of indices 1, …, m.  Since these premises all belong to T as well as to each of T1 , …,Tm, they belong to both T and ⊕{Ti}. So A is in T ∩ ⊕{Ti}.

The conditional

Informally, to begin.  To show that the calculus of classical theories is a Heyting algebra we need to identify the  → operation, to identify what is the weakest theory X such that T∩  X ⊆  T’.  If Y is that weakest theory,  that means that for all X, if  T∩ X ⊆  T’ then X ⊆  Y.  And of course, we would call it T  → T’.

The obvious candidate for Y is clearly the join of all the theories X such that T∩ X ⊆  T’.  But maybe that join is too weak?  We need to prove that it is still strong enough to play the role that T → T’ is meant to play.

Definition.  T → T’ = ⊕ {T’’: T ∩ T’’ ⊆  T’)  

Theorem.  T ∩ ⊕{T’’: T ∩ T’’ ⊆  T’)  ⊆ T’

Using the above result about infinite distributivity, and remembering the point about infinitary joins, we deduce:

             T ∩ ⊕{T’’: T ∩ T’’ ⊆  T’)  =  ⊕{T ∩ T”: T ∩ T’’ ⊆  T’)} ⊆ T’

To sum up:  (T → T’) as defined is in the set {T’’: T ∩ T’’ ⊆  T’), and is its weakest member, for it is the join of all the others.    

This completes the proof that the calculus of systems is a Heyting lattice.  This result holds for distributive logics generally, not just for classical logic.

There is still an interesting story to be told about the pseudo-complement ¬T and its relation to the complexities of infinity. 

That is for a sequel.

APPENDIX

Lemma.  If L is a distributive logic, then: if B ⊢L A and C, D ⊢L A then B v C, B v D ⊢L A

  1. B ⊢L A and C, D ⊢L A.                       Assume 
  2. (C &D) ⊢L A                                       1, [2]
  3. B v (C & D) ⊢L A                               1, 2, [1].
  4. B v C, B v D ⊢L  (B vC) & (B v D)    [2]
  5. (B v C) & (B v D) ⊢L B v (C & D)     [3]
  6. (B v C) & (B v D) ⊢L A                      3, 5

REFERENCES

Birkhoff, Garrett (1967)  Lattice Theory. (3rd edition) American Mathematical Society

McKinsey, J. C. C. and Alfred Tarski (1946) “On Closed Elements in Closure Algebras”. Annals of Mathematics 47: 122-162.

Tarski, Alfred (1935) “Foundations of the Calculus of Systems”.  Translation in Tarski (1956): 342-383.

Tarski, Alfred (1956) Logic, Semantics, Metamathematics. Oxford.

[i] Tarski does not provide a proof, but there is a proof of the dual result in McKinsey and Tarski (1946)