Anwendung der Logik Peter Ladkin

ladkin@techfak.uni-bielefeld.de
http://www.techfak.uni-bielefeld.de/~ladkin

[begin Administrativa] Ein Compendium-Beispiel (nicht Thema-Beispiel) für die Seminar-Arbeit steht unter

 http://www.techfak.uni-bielefeld.de/~ladkin

nämlich Computer-Related Incidents and Accidents with Commercial Airplanes Es ist ein Kompendium der schriftlichen Resourcen vom WWW über dieses Thema Die Bedürfnisse;

• Ein Thema auswählen

• relevante Resourcen im WWW und Bib suchen;

• Seminar-Vortrag/Vorschlag halten, um einen Kommentar von den anderen Teilnehmen zu bekommen;

• eine Zusammenfassung für das WWW:

kleine Einführung oder ‘Compendium’ schreiben.

Für die, die nichts über das WWW wissen, dieser Seminar könnte zusammen mit meinem WWW-Design Seminar (Fr 1200-1400) gebunden werden (4 WS im diesen Semester + nochmal 2WS → Prüfung)

[end Administrativa] Mögliche Arbeitsthemen:

• Verschiedene Arten von logischen Systemen

• Ein System und seine Anwendungen

• Logik in der Spezifikation

• Logik in der Verifikation

• Horn-Clause Logik - Logik-Programmierung • Konstruktive Logik

• Lineare Logik

• Lambek Kalkül

• Modale Logik

• Dynamische Logik

• Automated Theorem Provers (ATPs)

• Die Logik eines ATP Syntaktische Systeme der Logik

• Hilbertsche Systeme

• Natürliches Schließen

• Sequent-Kalkül

• Resolution

• Algebraische Methoden (Shostak, Nelson-Oppen, Knuth-Bendix-Rewriting-Systeme)

• Kombinatorische Logik Semantische Systeme der Logik

• Klassische Systeme

• Nicht-Klassische Systeme Nicht-Klassische Systeme der Logik

• Modale Logik

• Konstruktive Logik

• Inheritance-Systeme

• Type-Systeme

• Non-Monoton-Systeme

• Relevance Logik

• Lineare Logik

• Lambek-Kalkül Modale Logik

• Temporale Logik (Spezifikation, Verifikation, Handlungsplanung)

• Situation Calculus (Handlungsplanung)

• Belief/Knowledge Logik

• Montague Grammatik Konstruktive Logik

• Intuitionistische Logik • .... von höherer Ordnung • Manna-Waldinger Logik • NuPRL

• Lineare Logik Syntax of Logic

A logical system is based on a language which may be formal or natural

Examples: (formal) Propositional Logic First-Order Logic Higher-Order Logic Modal Logic

(natural)Deutsch English There are two aspects to the syntax of logic (good old data-structure stuff):

• Defining objects (well-formed formulas)

• Defining operations on objects (inference)

These are both normally defined as built by recursive functions from a recursive set (let’s just say finite set for the moment) of atoms

Atoms for wff’s are symbols

Atoms for inference are axioms The Semantics give the meaning of wff’s.

Semantics is often compositional that is, the meaning of the whole (formula) is determined by the meaning of the parts (subformulas)

We have a structure ⟨M , <⟩ where

• M is a set (of wff’s)

• < is a well-founded partial order on M

Then, for f ∈ M :

Meaning (f ) =^{Δ} F ({Meaning (g)|g < f })

where F is some function (let’s call it the semantic function)

Examples of compositional semantics: • Classical Propositional Logic

• Classical Predicate Logic

• Modal Logic

• Higher-Order Logic

• Sequential Programs (Floyd-Hoare logic)

Examples of non-compositional semantics:

• Brouwer’s (Heyting’s) Intuitionistic Logic

(many semantics, including the realisability semantics of Kleene/Friedman)

• Concurrent Programs

(Program 1 communicates with Program 2: how it functions is influenced by its environment, which includes Program 2, and not merely by the text of Program 1)

• Natural Language The reference of indexicals in a sentence (he, it, them) depends often on the context of a sentence. Meanings of sentences themselves often depend on the entire discourse

Nevertheless, one attempts to devise an equivalent system with a compositional semantics:

• Transformational grammar (Chomsky and many others)

• Montague grammar (Montague, then Partee and Dowty) It’s a higher-order modal logic Syntactical Styles

David Hilbert: Hilbert-style systems: logical axioms + simple inference rule

Gerhard Gentzen: Natural Deduction: no axioms; inference rules for each connective Untersuchungen über das logische Schliessen, Mathematische Zeitschrift 39, 1934, 176-210.

Sequent Calculus (also due to Gentzen): similar to a metatheory of ND. Axioms are A ⊢ A, where

A_{1}, A_{2}, ..., A_{m} ⊢ B_{1}, B_{2}, ..., B_{n}

is to be read as: if all of the A’s are true, then one of the B’s is true.

I shall use the formulation of Dag Prawitz in his book Natural Deduction, Almqvist and Wiksell, Stockholm 1965.

First, Well-Formed Formulas

First ingredient: a set of symbols

Symbols will usually include ( , ) , ∧ , ∨ , ⇒ , ¬ and symbols called propositional variables

One defines a set of meaningful strings, i.e., strings to which one assigns meaning: the well-formed formulae (wff’s)

(A ∧ B) is well-formed AB ∧ (( is not neither is (∧AB)

Usually, one uses parentheses around infix expressions, because they can have two different semantic interpretations c.f., A ∧ B ∨ C – do I mean (A ∧ B) ∨ C or A ∧ (B ∨ C ) ? But often one leaves them out In fact, if one uses prefix notation – ∧AB, ∨AB, ⇒ AB, ¬A one doesn’t need to use parentheses. There’s a unique reading of the formula This is called Polish notation. Here’s Reverse Polish: AB∧, AB∨, AB ⇒, ¬A And here’s Cambridge Polish (aka Lisp) (∧AB), (∨AB), (⇒ AB), (¬A) (why? because one mixes up symbols and their meanings, whereas in pure propositional logic the symbols have a precise sort – they’re variables or logical constants or punctuation)

A recursive definition of wff —

Every propositional variable is a wff (there’s an infinite fixed set of them)

If A is a wff then so is (¬A) If A and B are wffs then so is (A ∨ B) If A and B are wffs then so is (A ∧ B) If A and B are wffs then so is (A ⇒ B) If A and B are wffs then so is (A ≡ B)

Why do we want a recursive definition? How do recursive definitions work?

Recall that

Meaning (f ) =^{Δ} F ({Meaning (g)|g < f })

So if we want a compositional semantics, to find the meaning of a wff f , we can calculate the meaning of g for all g < f And so on.

But we must be assured we can stop.

We thus need the notion of a well-founded order < An order < is well-founded iff given any set S of things in the order, and any element y ∈ S, there is no infinite descending chain in S.

A chain in S is a totally-ordered subset of S. That is, a C = {x_{1}, x_{2}, ...., x_{n}, ...} ⊆ S such that ∀ x, y ∈ C : x ≤ y ∨ y ≤ x that is, one can arrange them somehow in an ordered line

... < x_{n} < x_{k} < x_{s} < ......

This is equivalent to saying that any descending chain C in S has a lower bound in C .

A lower bound x of a chain C in S is an element below all elements of C , i.e.,

x ∈ S ∧ ∀y ∈ C : x ≤ y

Consider the natural numbers ⟨N , <⟩ where N = {0, 1, 2, 3, 4, ....} < is well-founded (look at it)

Consider the integers ⟨I, <⟩ where I = {...., −2, −1, 0, 1, 2, 3, ....} < is not well-founded (look at it)

Induction is the rule

\frac{\begin{matrix}P(0) \\ ∀ n ∈ N : (P(n) ⇒ P(n + 1)) \end{matrix}}{∀ n ∈ N : P(n)}

Why is it true within ⟨N , <⟩?

Suppose the conclusion is false but the first premiss true

So S = { n | ¬P(n)} ≠ ∅ Pick m_{0}, its minimal element (exists by wfness)

m_{0} ≠ 0 (first premiss) so m_{0} − 1 exists Now ¬P(m_{0}) but P(m_{0} − 1) since m_{0} − 1 ∉ S which renders the second premiss false

with n = m_{0} − 1

So if both Premise 1 and Conclusion are true then Premise 2 is false

Hence if both Premises are true then Conclusion is true Hence the well-foundedness of < is used to show that induction is valid.

Induction is true also for any wf order < in a more general form.

\frac{∀ z ∈ S : minimal _{S}(z) ⇒ P(z) ∀ x ∈ S : (∀ y ∈ S : y < x ⇒ P(y)) ⇒ P(x)}{∀ x ∈ S : P(x)}

Here, minimal_{S}(z) is a predicate stating z is a minimal element of S

Induction justifies recursive definitions in particular for us, a recursive definition of semantics based on the construction of wff’s

Thus a compositional semantics with < interpreted as subformula of We started with the objects - wff’s Wff’s are sequences of symbols Now we consider sequences of wff’s and distinguish certain of them as proofs Inference, the Hilbert way

One starts off with a set of axioms Ax that is, wffs such as X ⇒ (Y ⇒ X ) where X , Y are propositional variables

... and three inference rules:

• Axiom (AX): \overline{A} where A ∈ AX

• Modus (Ponendo) Ponens (MP):

\frac{\begin{matrix}A \\ A ⇒ B \end{matrix}}{B}

• Substitution (SUB): \frac{A}{A[X /B]}

where A[X /B] denotes the formula obtained by replacing every occurrence of the propositional variable X in A by the wff B.

A proof is a sequence of wff’s such that each one is either an axiom or follows from earlier wff’s in the sequence by application of MP or SUB

This is (almost) a recursive definition if phrased right An example of SUB:

(X ⇒ (Y ⇒ X )[X /(X ∨ Y ), Y /(Z ⇒ X )] is defined to be (X ∨ Y ) ⇒ ((Z ⇒ X ) ⇒ (X ∨ Y ))

leading to the proof

\frac{(X ⇒ (Y ⇒ X )}{(X ∨ Y ) ⇒ ((Z ⇒ X ) ⇒ (X ∨ Y ))}

An example of MP:

\frac{(X ⇒ (Y ⇒ X )) (X ⇒ (Y ⇒ X )) ⇒ (Y ⇒ (X ⇒ (Y ⇒ X )))}{(Y ⇒ (X ⇒ (Y ⇒ X )))}

A theorem is the last wff in a proof There’s another way to characterise the proofs and the theorems

• Anything one can write down using the three rules is a proof (sufficiency).

• The only proofs are those sequences which can be obtained by doing this (necessity).

Here’s a restricted way to get the theorems (I interpret the rules as applying to a sequence of wffs to form a supersequence)

Let Inst be the transitive closure of Ax under SUB. It is easy to show Inst = {⟨D ⟩|∃ B ∈ wff , X ∈ PV, A ∈ Ax : D = A[X /B]}

Let Pf be the transitive closure of Inst under MP, and End (P) =^{Δ} P[Len(P)]

Then Thms = {A | ∃ P ∈ Pf : A = End (P)} Exercise: Show

Theorem: Thms is the set of theorems of propositional logic

Exercise: Let Mp be the transitive closure of Ax under MP and AX. (Mp is a set of sequences.) Let Sub be the transitive closure of Mp under SUB and AX. Show Sub ≠ Thms.

This is an instance of a general phenomenon, that sets characterised one way can be shown to be buildable by using other operations or the same operations in another order

Another example: Birkhoff’s Theorem which establishes the basis for equational logic and universal algebra So, wff’s and proofs may be considered as the transitive closure of a set under certain operations

When the operations are constructors that is, they retain the arguments somehow in the value (wff’s contain argument wff’s as subformulae; proofs contain the argument as initial segment) then induction over the constructors is valid for all objects in the transitive closure

For example, the formula-building function

A, B ↦ (A ∨ B)

is a constructor, since the arguments A and B form a part of the value (A ∨ B)

A binary truth function is not a constructor Why not? (Proof?)

What axiom systems are there for propositional logic?

A common set is

1: p ⇒ (q ⇒ p) 2: (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)) 3: ¬¬p ⇒ p

Church, Introduction to Mathematical Logic, Princeton UP, 1956 uses this in the form

C.3: ((p ⇒ ⊥) ⇒ ⊥) ⇒ p

because he defines ¬p to be (p ⇒ ⊥) where ⊥ is the logical constant whose value is always False Lukasiewicz 1930 uses 1, 2 and L.3: (¬p ⇒ ¬q) ⇒ (q ⇒ p)

Also, he suggests the set

L.II.1: (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r)) L.II.2: (¬p ⇒ p) ⇒ p L.II.3: p ⇒ (¬p ⇒ q)

A famous set comes from Whitehead and Russell, Principia Mathematica, vol. 1 Cambridge UP, 1910.

WR.1: (p ∨ p) ⇒ p WR.2: q ⇒ (p ∨ q) WR.3: (q ∨ p) ⇒ (p ∨ q) WR.4: (q ⇒ r) ⇒ ((p ∨ q) ⇒ (p ∨ r))

however, it’s not complete One must add to Whitehead and Russell’s axioms the following six, which introduce the other connectives

WR.5: (¬p ∨ q) ⇒ (p ⇒ q) WR.6: (p ⇒ q) ⇒ (¬p ∨ q) WR.7: (¬p ∨ ¬q) ⇒ ¬(p ∧ q) WR.8: ¬(p ∧ q) ⇒ (¬p ∨ ¬q) WR.9: (p ⇒ q) ∧ (q ⇒ p) ⇒ (p ≡ q) WR.10: (p ≡ q) ⇒ (p ⇒ q) ∧ (q ⇒ p)

Hilbert and Bernays, Grundlagen der Mathematik I, Zweite Auflage Springer 1968, p64 (1. Aufl. was 1934)

The king himself: Frege, Begriffschrift, 1879

1, 2, plus F.3: (p ⇒ (q ⇒ r)) ⇒ (q ⇒ (p ⇒ r)) F.4: (p ⇒ q) ⇒ (¬q ⇒ ¬p) F.5: p ⇒ ¬¬p F.6: ¬¬p ⇒ p

A single axiom suffices! S. Lesniewski, Grundzüge eines neuen Systems der Grundlagen der Mathematik, Fundamenta Mathematica 14 (1929)

Also with the Sheffer stroke, with rule \frac{\begin{matrix}A \\ A|(B|C ) \end{matrix}}{C}

(Nicod, A reduction in the number of primitive propositions of logic, Proc. Camb. Phil. Soc. 19, 1917)

Hilbert, Grundlagen der Geometrie, 1900 (also in Hilbert-Bernays, p69)

H.I. Implication 1. p ⇒ (q ⇒ p)

2. (p ⇒ (p ⇒ q)) ⇒ (p ⇒ q)

3. (p ⇒ q) ⇒

((q ⇒ r) ⇒ (p ⇒ r))

H.II. Conjunction 1. p ∧ q ⇒ p)

2. p ∧ q ⇒ q

3. (p ⇒ q) ⇒

((p ⇒ r) ⇒ (p ⇒ (q ∧ r)))

H.III. Disjunction 1. p ⇒ (p ∨ q)

2. q ⇒ (p ∨ q)

3. (p ⇒ r) ⇒

((q ⇒ r) ⇒ (p ∨ r ⇒ r))

H.IV. Equivalence 1. (p ≡ q) ⇒ (p ⇒ q) 2. (p ≡ q) ⇒ (q ⇒ p)

3. (p ⇒ q) ⇒

((q ⇒ p) ⇒ (p ≡ q)

Note I.3 is identical to 4 Hilbert’s axioms (cont’d) V. Negation 1. (p ⇒ q) ⇒ (¬q ⇒ ¬p)

2. p ⇒ ¬¬p

3. ¬¬p ⇒ p

Kleene, Introduction to Metamathematics North-Holland 1971 (6th reprint of 1952 edition) gives

K.1.a: p ⇒ (q ⇒ p) K.1.b: (p ⇒ q) ⇒ ((p ⇒ (q ⇒ r)) ⇒ (p ⇒ r)) K.2: MP (it’s a rule!) K.3: p ⇒ (q ⇒ (p ∧ q)) K.4.a: p ∧ q ⇒ p K.4.b: p ∧ q ⇒ q K.5.a: p ⇒ p ∨ q K.5.b: q ⇒ p ∨ q K.6: (p ⇒ r) ⇒ ((q ⇒ r) ⇒ (p ∨ q ⇒ r)) K.7: (p ⇒ q) ⇒ ((p ⇒ ¬q) ⇒ ¬p) K.8: ¬¬p ⇒ p

Note that many of these have occurred before

If K.8 is replaced by K.9: ¬p ⇒ (p ⇒ q) then the system corresponds to intuitionistic propositional logic Also, one can translate the axioms of Boolean Algebra into logic: there are two binary operations ∧, ∨ and a unary ¬.

15, 16 ∧, ∨ are associative 17, 18 ∧, ∨ are commutative 19, 20 ∧, ∨ distribute over each other 21, 22: (p ∨ q) ∧ p = p, (p ∧ q) ∨ p = p 23, 24: (p ∨ p) = p, (p ∧ p) = p 25, 26: p ∨ ¬p = 1, p ∧ ¬p = 0 27-30: p ∧ 1 = p, p ∨ 1 = 1, p ∨ 0 = p, p ∧ 0 = 0 31, 32: ¬(p∧q) = (¬p∨¬q), ¬(p∨q) = (¬p∧¬q)

One translates X = Y into (X ⇒ Y )∧(Y ⇒ X ) Either ⊤, ⊥ are logical constants, or add ⊥ and define ⊤ as ¬⊥ or define ⊥ as p ∧ ¬p (read this as a bootstrap)

Semantics

The semantics for classical propositional logic bases itself on truth values (Wittgenstein, Logisch-Philosophische Abhandlungen)

Propositions (wff’s) can be either True or False (T or F; 1 or 0; ⊤ or ⊥)

Semantics is compositional the relation subformula of is well-founded so we may use a recursive definition starting with the minimal subformulas, i.e., the propositional variables

One assigns truth values to the propositional variables and a recursive definition of truth value assigns each wff a truth value

That is, for each clause of the recursive definition of formula, one says how the result is true or false, given the possible values of its arguments Operations: A, B ↦ (A ∨ B)

A, B ↦ (A ∧ B)

A, B ↦ (A ⇒ B)
A ↦ (¬A)

So, A, B must be given their possible values (⊤, ⊥) and we must say what value (A op B) has

This specifies (A op B) as a binary function of these arguments

The arguments are truth-values as are the results

Hence these are truth functions and we have a truth-functional semantics Tautologies are wff’s which are always true no matter what values the variables take, e.g.,

A ⇒ ( B ⇒ A) T T T T T T T F T T F T T F F F T F T F

I got this table by considering all the possible combinations of T and F for A and B, and combining them using the basic Truth Tables for the connectives Here are the truth tables for two connectives

A B ∥ A ∨ B T T ∥ T T F ∥ T F T ∥ T F F ∥ F

A ∥ ¬A F ∥ T T ∥ F

These are tables giving all possible values of the function for all possible arguments

This is possible because the functions only have finitely many argument combinations and therefore only finitely many values But I only gave the truth tables for one unary and one binary truth function Why? Because they form a complete set of truth functions That is, all binary truth functions may be obtained by composition from these two. That says that all possible truth tables may be obtained by combining these two Can you prove this statement above? How many such functions are there?

OK, OK, here are the truth tables for the other two connectives

A B ∥ A ∧ B T T ∥ T T F ∥ F F T ∥ F F F ∥ F

A B ∥ A ⇒ B T T ∥ T T F ∥ F F T ∥ T F F ∥ T In fact, here’s an even better exercise

Prove that you can obtain all unary and binary truth functions from the single

A B ∥ A | B T T ∥ F T F ∥ F F T ∥ F F F ∥ T

This is called Joint Denial or Sheffer Stroke, Sheffer’s only notable contribution to logic, used by both Wittgenstein and Russell Semantics: what it means, what you’re trying to calculate by doing inference

All the axioms of Hilbert-style propositional logic are tautologies

and the rules MP, SUB preserve tautologies, that is,

(MP) if A is a tautology and A ⇒ B is a tautology then so is B

(SUB) if A is a tautology, then so is A[X /B]

Check this.

Thus, all theorems of Hilbert-style logic are tautologies But are all tautologies also theorems of Hilbert-style logic? Yes. This is called the Completeness Theorem for Hilbert-style propositional logic You could perhaps prove it? (Looking it up is easier)

But I’m going to do Prawitz-style Gentzen-style natural deduction

Prawitz has fewer axioms

In fact, he doesn’t have any

But he has lots of rules — introduction and elimination rules for each logical constant (operator of propositional logic)

And he has a way of marking formulae as assumptions early in a proof and discharging them later In a natural deduction, one assumes certain formulae, and then uses the rules to prove other formulae. One may write an already written formula or a substitution instance thereof or one may write a formula which is an instance of a conclusion of a rule of which one has already written the instances

There are ways in which assumptions may be discharged (eliminated)

A theorem is a formula obtained by a proof in which all assumptions have been discharged Here’s a proof of a theorem:

\frac{{[A] \atop A}}{A ⇒ A}

Here, [A] indicates an assumption of A that has been later discharged

This proof of A ⇒ A is an instance of the rule ⇒-introduction:

\frac{{[A] \atop B}}{A ⇒ B}

This says, from A and B, write A ⇒ B and discharge all occurences of A above Here’s a proof of the Hilbert axiom A ⇒ (B ⇒ A) using this rule:

\frac{\begin{matrix}[B] \\ [A] \\ B ⇒ A \end{matrix}}{A ⇒ (B ⇒ A)}

(I’m messing around with parentheses to make it more readable)

Here, B is assumed, then A. B ⇒ A is concluded,

discharging assumptions of B Finally, A ⇒ (B ⇒ A) is concluded,

discharging assumptions of A.

So there are no assumptions left, and the conclusion is thus a theorem So what (propositional) rules are there?

(&-intro) \frac{A B}{A ∧ B} (&-elim) \frac{A ∧ B}{A} \frac{A ∧ B}{B}

(∨-intro) \frac{A}{A ∨ B} \frac{A}{A ∨ B}

(∨-elim)

A ∨ B [A] [B]

\frac{C C}{C}

Note that these rules build proof trees, not sequences, since proof branches converge in certain rules. The root is the theorem.

(⇒-intro) \frac{{[A] \atop B}}{A ⇒ B} (⇒-elim) \frac{A A ⇒ B}{B}

(¬A) is defined to be the formula (A ⇒ ⊥)

(⊥l) \frac{⊥}{A} (⊥c) \frac{\begin{matrix}[¬A] \\ ⊥ \end{matrix}}{A}

A restriction on both ⊥ rules is that A is different from ⊥

A restriction on ⊥c is that A is not of the form B ⇒ ⊥ This is only for convenience

Show that if A has the form ¬B in ⊥c that there’s another way of deriving the conclusion Note that ⊥c subsumes ⊥l

If ⊥c is used, the theorems are those of classical propositional logic

If ⊥l is used, the theorems are those of intuitionistic propositional logic

The difference is just that of how negation is treated

Compare with Kleene’s axiomatisation of propositional logic which includes K.8: ¬¬p ⇒ p. If one replaces K.8 with K.9: ¬q ⇒ (p ⇒ q), intuitionistic propositional logic results Gentzen-style natural deduction is also complete. That is, the theorems are precisely the tautologies

An exercise: as before, show that the rules preserve tautologies (um, except for the ⊥-rules)

Gentzen-style proofs are written as a tree with the conclusion as root. Assumptions are discharged on all branches above a given node (conclusion)

But one may write these trees linearly. Here’s a recursive definition (a little hidden) One may write the conclusion first, and the premises in (arbitrary) linear order below. Below each premise, and before the next, occurs the proof of this premise

This is Lamport’s hierarchical method Here are the Lamport-hierarchical versions of the rules, as used in TLA proofs

⟨1⟩1. A ∧ B Proof: ⟨2⟩1. A ⟨2⟩2. B ⟨2⟩3. Q.E.D.

Proof: &-intro.

⟨1⟩1. A Proof: ⟨2⟩1. A ∧ B ⟨2⟩2. Q.E.D.

Proof: &-elim-left.

⟨1⟩1. B Proof: ⟨2⟩1. A ∧ B ⟨2⟩2. Q.E.D.

Proof: &-elim-right.

⟨1⟩1. A ⇒ B Proof:

ASSUME A PROVE B

⟨2⟩1. B

Proof: (Use A freely). ⟨2⟩2. Q.E.D.

Proof: ⇒-intro.

⟨1⟩1. B Proof: ⟨2⟩1. A ⟨2⟩2. A ⇒ B ⟨2⟩3. Q.E.D.

Proof: ⇒-elim.

⟨1⟩1. A ∨ B Proof: ⟨2⟩1. A ⟨2⟩2. Q.E.D.

Proof: ∨-intro-left.

⟨1⟩1. A ∨ B Proof: ⟨2⟩1. B ⟨2⟩2. Q.E.D.

Proof: ∨-intro-right.

⟨1⟩1. C Proof: ⟨2⟩1. A ∨ B ⟨2⟩2. A ⇒ C ⟨2⟩3. B ⇒ C ⟨2⟩4. Q.E.D.

Proof: ∨-elim.

How did I do this? Notice that from \underline{\begin{matrix}[A] \\ . \\ C \end{matrix}}

we may simply conclude \overline{A ⇒ C} by ⇒-I

so that if I may prove the former, I may also prove the latter. I just added this extra step for both \underline{\begin{matrix}[A] \\ . \\ C \end{matrix}} and \underline{\begin{matrix}[B] \\ . \\ C \end{matrix}} Here are the two ⊥ rules

One or the other needs to be included depending on what logic you want

⟨1⟩1. A Proof: ⟨2⟩1. ⊥ ⟨2⟩2. Q.E.D.

Proof: ⊥l.

⟨1⟩1. A Proof:

ASSUME A ⇒ ⊥ PROVE ⊥

⟨2⟩1. ⊥

Proof: (Use A ⇒ ⊥ freely). ⟨2⟩2. Q.E.D.

Proof: ⊥c.

In principle, by using these rules and these rules only, you will be able to prove all the tautologies and do any propositional inference that you need to

The End