A language L for Arithmetic. The judgement tree.

The Language L. We consider the language L for arithmetic, having one constant symbol n for each natural number, one predicate symbol p for each computable predicate (for instance: = (equality), ≤, ≥, ≠, ...), one function symbol f for each computable function (for instance: a polynomial in x). Formulas are all first order formulas in the logical constant T, F, and the connectives ∧, ∨, →, ¬, ∀, ∃ (with quantifiers ranging over natural numbers).
Atoms. We call a formula without connectives (say, T, F, x ≤ 3) an atomic formula, or an atom, for short.
A judgement is a statement t.A or f.A, to be read: ``A is true'', ``A is false''. We call t., f. the sign of the judgment. The sign t. is a positive sign, and t.A a positive judgment. The sign f.A is a negative sign, and f.A a negative judgement. A formula F and a judgement t.F are essentially identified.

Material Implication. In this site, unless otherwise stated, the intended meaning of negation is De' Morgan dual: the meaning of ¬A is the formula obtained by switching ∧ with ∨, and ∀ with ∃, and each computable predicate p with its complement ¬p. Unless otherwise stated, the meaning of the implication is material implication: ``A implies B'' means ``either A is false, or B is true''. In other words, A→B is, essentially, ¬A∨B.

Constructive Implication. Later on, we will also consider a language LCons with constructive negation and implication. In LCons, the intended meaning of ¬A is: ``in all possible worlds, if we assume A we derive a contradiction''. In LCons, we write implication as A⇒B, instead of A→B. The intended meaning of ``A⇒B'' is: `if we assume A we derive B''. A→B and A⇒B are equivalent if we have full classical logic, but many proofs (even many classical proofs) becomes shorter and simpler if we take the constructive meaning of negation and of implication. This is why we will also consider game semantic for constructive negation and implication, but only later, in another section of this site. In this section, the language is L, and implication is material implication.

Subjudgements. If A is closed, and made of "parts" A', A", ..., we think that also the judgement t.A is made of "parts" t.A', t.A", ..., and the judgement the judgement f.A is made of "parts" f.A', f.A", ... . We call a "part" an immediate subjudgement. Usually the sign of a judgement and of an immediate subjudgement are the same, but in a few cases, marked by a * below, the sign changes.
The formal definition of immediate subjudgement runs as follows.
   1. t.T, t.F, f.T, f.F have no immediate subjudgements.
   2. t.a,  with a atomic ≠ T, F, has immediate subjudgement t.T if a is true, and t.F if a is false.
       f.a, with a atomic ≠ T, F, has immediate subjudgement f.T if a is true, and f.F if a is false.
   3. t.A∧B, t.A∨B have immediate subjudgements t.A and t.B, while f.A∧B, f.A∨B have immediate subjudgements f.A and f.B.
*4. t.A→B has immediate subjudgements f.A and t.B, while f.A→B has immediate subjudgements t.A, f.B. Here the sign of A changes.
*5.  t.¬A has immediate subjudgement f.A, while f.¬A has immediate subjudgements t.A. Here the sign of A changes.
  6. t.∀x.A, t.∃x.A have immediate subjudgements t.A[t/x], for all closed terms t, while f.∀x.A, f.∃x.A have immediate subjudgements f.A[t/x], for all closed t.
The subjudgements of t.A or f.A are all immediate subjudgements, all immediate subjudgements of all immediate subjudgements, and so forth.

Judgement tree. The judgement tree of t.A (or f.A) is the tree the sub-judgement relation for A. The tree has one node for each subjudgement of t.A (or f.A), and one edge for any two subjudgements, one immediate subjudgement of the other. The judgement tree of A is the judgement tree of t.A.

This is the judgement tree of t.((A∧B)∨((A∧¬B)∨(¬A∧B))), cut down to the nodes t.A,t.B,f.A, f.B.  

We could have some more nodes below the nodes t.A, t.B, f.A, f.B.

Created by Mathematica  (October 17, 2006)