This article needs additional citations for verification . (April 2010) (Learn how and when to remove this template message) |
System L is a natural deductive logic developed by E.J. Lemmon. [1] Derived from Suppes' method, [2] it represents natural deduction proofs as sequences of justified steps. Both methods are derived from Gentzen's 1934/1935 natural deduction system, [3] in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical applications.
A similar tabular layout is presented by Kleene. [4] The main difference is that Kleene does not abbreviate the left-hand sides of assertions to line numbers, preferring instead to either give full lists of precedent propositions or alternatively indicate the left-hand sides by bars running down the left of the table to indicate dependencies. However, Kleene's version has the advantage that it is presented, although only very sketchily, within a rigorous framework of metamathematical theory, whereas the books by Suppes [2] and Lemmon [1] are applications of the tabular layout for teaching introductory logic.
System L is a predicate calculus with equality, so its description can be separated into two parts: the general proof syntax and the context specific rules.
A proof is a table with 4 columns and unlimited ordered rows. From left to right the columns hold:
The following is an example:
p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)] | |||
Assumption number | Line number | Formula (wff) | Lines in-use and Justification |
---|---|---|---|
1 | (1) | p → q | A |
2 | (2) | ¬q | A |
3 | (3) | p | A (for RAA) |
1, 3 | (4) | q | 1, 3, MPP |
1, 2, 3 | (5) | q ∧ ¬q | 2, 4, ∧I |
1, 2 | (6) | ¬p | 3, 5, RAA |
Q.E.D |
The second column holds line numbers. The third holds a wff, which is justified by the rule held in the fourth along with auxiliary information about other wffs, possibly in other proofs. The first column represents the line numbers of the assumptions the wff rests on, determined by the application of the cited rule in context. Any line of any valid proof can be converted into a sequent by listing the wffs at the cited lines as the premises and the wff at the line as the conclusion. Analogously, they can be converted into conditionals where the antecedent is a conjunction. These sequents are often listed above the proof, as Modus Tollens is above.
The above proof is a valid one, but proofs don't need to be to conform to the general syntax of the proof system. To guarantee a sequent's validity, however, we must conform to carefully specified rules. The rules can be divided into four groups: the propositional rules (1-10), the predicate rules (11-14), the rules of equality (15-16), and the rule of substitution (17). Adding these groups in order allows one to build a propositional calculus, then a predicate calculus, then a predicate calculus with equality, then a predicate calculus with equality allowing for the derivation of new rules. Some of the propositional calculus rules, like MTT, are superfluous and can be derived as rules from other rules.
An example of the proof of a sequent (a theorem in this case):
⊢p ∨ ¬p | |||
Assumption number | Line number | Formula (wff) | Lines in-use and Justification |
---|---|---|---|
1 | (1) | ¬(p ∨ ¬p) | A (for RAA) |
2 | (2) | p | A (for RAA) |
2 | (3) | (p ∨ ¬p) | 2, ∨I |
1, 2 | (4) | (p ∨ ¬p) ∧ ¬(p ∨ ¬p) | 3, 1, ∧I |
1 | (5) | ¬p | 2, 4, RAA |
1 | (6) | (p ∨ ¬p) | 5, ∨I |
1 | (7) | (p ∨ ¬p) ∧ ¬(p ∨ ¬p) | 1, 6, ∧I |
(8) | ¬¬(p ∨ ¬p) | 1, 7, RAA | |
(9) | (p ∨ ¬p) | 8, DN | |
Q.E.D | |||
A proof of the principle of explosion using monotonicity of entailment. Some have called the following technique, demonstrated in lines 3-6, the Rule of (Finite) Augmentation of Premises: [5]
p, ¬p ⊢ q | |||
Assumption number | Line number | Formula (wff) | Lines in-use and Justification |
---|---|---|---|
1 | (1) | p | A (for RAA) |
2 | (2) | ¬p | A (for RAA) |
1, 2 | (3) | p ∧ ¬p | 1, 2, ∧I |
4 | (4) | ¬q | A (for DN) |
1, 2, 4 | (5) | (p ∧ ¬p) ∧ ¬q | 3, 4, ∧I |
1, 2, 4 | (6) | p ∧ ¬p | 5, ∨E |
1, 2 | (7) | ¬¬q | 4, 6, RAA |
1, 2 | (8) | q | 7, DN |
Q.E.D |
An example of substitution and ∨E:
(p ∧ ¬p) ∨ (q ∧ ¬q) ⊢ r | |||
Assumption number | Line number | Formula (wff) | Lines in-use and Justification |
---|---|---|---|
1 | (1) | (p ∧ ¬p) ∨ (q ∧ ¬q) | A |
2 | (2) | p ∧ ¬p | A (for ∨E) |
2 | (3) | p | 2 ∧E |
2 | (4) | ¬p | 2 ∧E |
2 | (5) | r | 3, 4 SI(S) see above proof |
6 | (6) | q ∧ ¬q | A (for ∨E) |
6 | (7) | q | 6 ∧E |
6 | (8) | ¬q | 2 ∧E |
6 | (9) | r | 7, 8 SI(S) see above proof |
1 | (10) | r | 1, 2, 5, 6, 9, ∨E |
Q.E.D |
The historical development of tabular-layout natural deduction systems, which are rule-based, and which indicate antecedent propositions by line numbers (and related methods such as vertical bars or asterisks) includes the following publications.
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives. Propositions that contain no logical connectives are called atomic propositions.
In propositional logic, modus ponens, also known as modus ponendo ponens or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "P implies Q.P is true. Therefore Q must also be true."
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
In classical logic, hypothetical syllogism is a valid argument form which is a syllogism having a conditional statement for one or both of its premises.
Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics.
A rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion. For example, the rule of inference called modus ponens takes two premises, one in the form "If p then q" and another in the form "p", and returns the conclusion "q". The rule is valid with respect to the semantics of classical logic, in the sense that if the premises are true, then so is the conclusion.
Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the style of natural deduction used by mathematicians than David Hilbert's earlier style of formal logic where every line was an unconditional tautology. There may be more subtle distinctions to be made; for example, there may be non-logical axioms upon which all propositions are implicitly dependent. Then sequents signify conditional theorems in a first-order language rather than conditional tautologies.
In mathematical logic, a sequent is a very general kind of conditional assertion.
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can be identified with the set of formulas in the language.
In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs — to prove an implication A → B, assume A as an hypothesis and then proceed to derive B — in systems that do not have an explicit inference rule for this. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule.
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional formula may also be called a propositional expression, a sentence, or a sentential formula.
In propositional logic, transposition is a valid rule of replacement that permits one to switch the antecedent with the consequent of a conditional statement in a logical proof if they are also both negated. It is the inference from the truth of "A implies B" the truth of "Not-B implies not-A", and conversely. It is very closely related to the rule of inference modus tollens. It is the rule that:
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.
In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules. Frege systems are named after Gottlob Frege.