It makes use of just two logical operators: implication and negation, and it is constituted by six axioms and one inference rule: modus ponens.
Axioms
Inference Rule
THEN-1
A → (B → A)
THEN-2
(A → (B → C)) → ((A → B) → (A → C))
THEN-3
(A → (B → C)) → (B → (A → C))
FRG-1
(A → B) → (¬B → ¬A)
FRG-2
¬¬A → A
FRG-3
A → ¬¬A
MP
P, P→Q ⊢ Q
Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN-1 and THEN-2. Notice that axioms THEN-1 through THEN-3 only make use of (and define) the implication operator, whereas axioms FRG-1 through FRG-3 define the negation operator.
The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem-space" of Frege's PC, showing that the theory of standard PC is contained within the theory of Frege's PC.
(A theory, also called here, for figurative purposes, a "theorem-space", is a set of theorems that are a subset of a universal set of well-formed formulas. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem-space are found the axioms, which "generate" the theorem-space much like a generating set generates a group.)
Rules
Rule(THEN-1)—A ⊢ B→A
#
wff
reason
1.
A
premise
2.
A→(B→A)
THEN-1
3.
B→A
MP 1,2.
Rule(THEN-2)— A→(B→C) ⊢ (A→B)→(A→C)
#
wff
reason
1.
A→(B→C)
premise
2.
(A → (B → C)) → ((A → B) → (A → C))
THEN-2
3.
(A→B)→(A→C)
MP 1,2.
Rule(THEN-3)—A→(B→C) ⊢ B→(A→C)
#
wff
reason
1.
A→(B→C)
premise
2.
(A → (B → C)) → (B → (A → C))
THEN-3
3.
B→(A→C)
MP 1,2.
Rule(FRG-1)—A→B ⊢ ¬B→¬A
#
wff
reason
1.
(A→B)→(¬B→¬A)
FRG-1
2.
A→B
premise
3.
¬B→¬A
MP 2,1.
Rule(TH1)— A→B, B→C ⊢ A→C
#
wff
reason
1.
B→C
premise
2.
(B→C)→(A→(B→C))
THEN-1
3.
A→(B→C)
MP 1,2
4.
(A→(B→C))→((A→B)→(A→C))
THEN-2
5.
(A→B)→(A→C)
MP 3,4
6.
A→B
premise
7.
A→C
MP 6,5.
Theorems
Theorem(TH1)—(A→B)→((B→C)→(A→C))
#
wff
reason
1.
(B→C)→(A→(B→C))
THEN-1
2.
(A→(B→C))→((A→B)→(A→C))
THEN-2
3.
(B→C)→((A→B)→(A→C))
TH1* 1,2
4.
((B→C)→((A→B)→(A→C)))→((A→B)→((B→C)→(A→C)))
THEN-3
5.
(A→B)→((B→C)→(A→C))
MP 3,4.
Theorem(TH2)—A→(¬A→¬B)
#
wff
reason
1.
A→(B→A)
THEN-1
2.
(B→A)→(¬A→¬B)
FRG-1
3.
A→(¬A→¬B)
TH1* 1,2.
Theorem(TH3)—¬A→(A→¬B)
#
wff
reason
1.
A→(¬A→¬B)
TH 2
2.
(A→(¬A→¬B))→(¬A→(A→¬B))
THEN-3
3.
¬A→(A→¬B)
MP 1,2.
Theorem(TH4)—¬(A→¬B)→A
#
wff
reason
1.
¬A→(A→¬B)
TH3
2.
(¬A→(A→¬B))→(¬(A→¬B)→¬¬A)
FRG-1
3.
¬(A→¬B)→¬¬A
MP 1,2
4.
¬¬A→A
FRG-2
5.
¬(A→¬B)→A
TH1* 3,4.
Theorem(TH5)—(A→¬B)→(B→¬A)
#
wff
reason
1.
(A→¬B)→(¬¬B→¬A)
FRG-1
2.
((A→¬B)→(¬¬B→¬A))→(¬¬B→((A→¬B)→¬A))
THEN-3
3.
¬¬B→((A→¬B)→¬A)
MP 1,2
4.
B→¬¬B
FRG-3, with A:= B
5.
B→((A→¬B)→¬A)
TH1* 4,3
6.
(B→((A→¬B)→¬A))→((A→¬B)→(B→¬A))
THEN-3
7.
(A→¬B)→(B→¬A)
MP 5,6.
Theorem(TH6)—¬(A→¬B)→B
#
wff
reason
1.
¬(B→¬A)→B
TH4, with A:= B, B:= A
2.
(B→¬A)→(A→¬B)
TH5, with A:= B, B:= A
3.
((B→¬A)→(A→¬B))→(¬(A→¬B)→¬(B→¬A))
FRG-1
4.
¬(A→¬B)→¬(B→¬A)
MP 2,3
5.
¬(A→¬B)→B
TH1* 4,1.
Theorem(TH7)—A→A
#
wff
reason
1.
A→¬¬A
FRG-3
2.
¬¬A→A
FRG-2
3.
A→A
TH1* 1,2.
Theorem(TH8)—A→((A→B)→B)
#
wff
reason
1.
(A→B)→(A→B)
TH7, with A:= A→B
2.
((A→B)→(A→B))→(A→((A→B)→B))
THEN-3
3.
A→((A→B)→B)
MP 1,2.
Theorem(TH9)—B→((A→B)→B)
#
wff
reason
1.
B→((A→B)→B)
THEN-1, with A:= B, B:= A→B.
Theorem(TH10)—A→(B→¬(A→¬B))
#
wff
reason
1.
(A→¬B)→(A→¬B)
TH7
2.
((A→¬B)→(A→¬B))→(A→((A→¬B)→¬B)
THEN-3
3.
A→((A→¬B)→¬B)
MP 1,2
4.
((A→¬B)→¬B)→(B→¬(A→¬B))
TH5
5.
A→(B→¬(A→¬B))
TH1* 3,4.
Note: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), and A→(B→¬(A→¬B)) (TH10), so ¬(A→¬B) behaves just like A∧B (compare with axioms AND-1, AND-2, and AND-3).
Note: A→((A→B)→B) (TH8), B→((A→B)→B) (TH9), and (A→C)→((B→C)→(((A→B)→B)→C)) (TH19), so ((A→B)→B) behaves just like A∨B. (Compare with axioms OR-1, OR-2, and OR-3.)
Theorem(TH20)—(A→¬A)→¬A
#
wff
reason
1.
(A→A)→((A→¬A)→¬A)
TH11
2.
A→A
TH7
3.
(A→¬A)→¬A
MP 2,1.
TH20 corresponds to axiom NOT-3 of standard PC, called "tertium non datur".
All the axioms of standard PC have been derived from Frege's PC, after having let
Rule($1)—$2
A∧B:= ¬(A→¬B) and A∨B:= (A→B)→B. These expressions are not unique, e.g. A∨B could also have been defined as (B→A)→A, ¬A→B, or ¬B→A. Notice, though, that the definition A∨B:= (A→B)→B contains no negations. On the other hand, A∧B cannot be defined in terms of implication alone, without using negation.
In a sense, the expressions A∧B and A∨B can be thought of as "black boxes". Inside, these black boxes contain formulas made up only of implication and negation. The black boxes can contain anything, as long as when plugged into the AND-1 through AND-3 and OR-1 through OR-3 axioms of standard PC the axioms remain true. These axioms provide complete syntactic definitions of the conjunction and disjunction operators.
The next set of theorems will aim to find the remaining four axioms of Frege's PC within the "theorem-space" of standard PC, showing that the theory of Frege's PC is contained within the theory of standard PC.
Theorem(ST1)—A→A
#
wff
reason
1.
(A→((A→A)→A))→((A→(A→A))→(A→A))
THEN-2
2.
A→((A→A)→A)
THEN-1
3.
(A→(A→A))→(A→A)
MP 2,1
4.
A→(A→A)
THEN-1
5.
A→A
MP 4,3.
Theorem(ST2)—A→¬¬A
#
wff
reason
1.
A
hypothesis
2.
A→(¬A→A)
THEN-1
3.
¬A→A
MP 1,2
4.
¬A→¬A
ST1
5.
(¬A→A)→((¬A→¬A)→¬¬A)
NOT-1
6.
(¬A→¬A)→¬¬A
MP 3,5
7.
¬¬A
MP 4,6
8.
A ⊢ ¬¬A
summary 1-7
9.
A→¬¬A
DT 8.
ST2 is axiom FRG-3 of Frege's PC.
Theorem(ST3)—B∨C→(¬C→B)
#
wff
reason
1.
C→(¬C→B)
NOT-2
2.
B→(¬C→B)
THEN-1
3.
(B→(¬C→B))→ ((C→(¬C→B))→((B ∨ C)→(¬C→B)))
OR-3
4.
(C→(¬C→B))→((B ∨ C)→(¬C→B))
MP 2,3
5.
B∨C→(¬C→B)
MP 1,4.
Theorem(ST4)—¬¬A→A
#
wff
reason
1.
A∨¬A
NOT-3
2.
(A∨¬A)→(¬¬A→A)
ST3
3.
¬¬A→A
MP 1,2.
ST4 is axiom FRG-2 of Frege's PC.
Prove ST5: (A→(B→C))→(B→(A→C))
#
wff
reason
1.
A→(B→C)
hypothesis
2.
B
hypothesis
3.
A
hypothesis
4.
B→C
MP 3,1
5.
C
MP 2,4
6.
A→(B→C), B, A ⊢ C
summary 1-5
7.
A→(B→C), B ⊢ A→C
DT 6
8.
A→(B→C) ⊢ B→(A→C)
DT 7
9.
(A→(B→C)) → (B→(A→C))
DT 8.
ST5 is axiom THEN-3 of Frege's PC.
Theorem(ST6)—(A→B)→(¬B→¬A)
#
wff
reason
1.
A→B
hypothesis
2.
¬B
hypothesis
3.
¬B→(A→¬B)
THEN-1
4.
A→¬B
MP 2,3
5.
(A→B)→((A→¬B)→¬A)
NOT-1
6.
(A→¬B)→¬A
MP 1,5
7.
¬A
MP 4,6
8.
A→B, ¬B ⊢ ¬A
summary 1-7
9.
A→B ⊢ ¬B→¬A
DT 8
10.
(A→B)→(¬B→¬A)
DT 9.
ST6 is axiom FRG-1 of Frege's PC.
Each of Frege's axioms can be derived from the standard axioms, and each of the standard axioms can be derived from Frege's axioms. This means that the two sets of axioms are interdependent and there is no axiom in one set that is independent from the other set. Therefore, the two sets of axioms generate the same theory: Frege's PC is equivalent to standard PC.
(For if the theories should be different, then one of them should contain theorems not contained by the other theory. These theorems can be derived from their own theory's axiom set: but as has been shown this entire axiom set can be derived from the other theory's axiom set, which means that the given theorems can actually be derived solely from the other theory's axiom set, so that the given theorems also belong to the other theory. Contradiction: thus the two axiom sets span the same theorem-space. By construction: Any theorem derived from the standard axioms can be derived from Frege's axioms, and vice versa, by first proving as theorems the axioms of the other theory as shown above and then using those theorems as lemmas to derive the desired theorem.)
An axiom, postulate or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Greek axíōma (ἀξίωμα) 'that which is thought worthy or fit' or 'that which commends itself as evident.'
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.
In logic, a logical connective is a logical constant used to connect two or more formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .
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.
The Principia Mathematica is a three-volume work on the foundations of mathematics written by the mathematicians Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. In 1925–27, it appeared in a second edition with an important Introduction to the Second Edition, an Appendix A that replaced ✸9 and all-new Appendix B and Appendix C. PM is not to be confused with Russell's 1903 The Principles of Mathematics. PM was originally conceived as a sequel volume to Russell's 1903 Principles, but as PM states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of Principles of Mathematics... But as we advanced, it became increasingly evident that the subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions."
The history of logic deals with the study of the development of the science of valid inference (logic). Formal logics developed in ancient times in India, China, and Greece. Greek methods, particularly Aristotelian logic as found in the Organon, found wide application and acceptance in Western science and mathematics for millennia. The Stoics, especially Chrysippus, began the development of predicate logic.
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.
In mathematics and logic, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A theory is a consistent, relatively-self-contained body of knowledge which usually contains an axiomatic system and all its derived theorems. An axiomatic system that is completely described is a special kind of formal system. A formal theory is an axiomatic system that describes a set of sentences that is closed under logical implication. A formal proof is a complete rendition of a mathematical proof within a formal system.
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.
In mathematical logic, 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 natural style of 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.
A formal system is used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A formal system is essentially an "axiomatic system".
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.
In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them. Syntax is concerned with the rules used for constructing, or transforming the symbols and words of a language, as contrasted with the semantics of a language which is concerned with its meaning.
Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book.
In mathematical logic, a proof calculus or a proof system is built to prove statements.
In metalogic and metamathematics, Frege's theorem is a metatheorem that states that the Peano axioms of arithmetic can be derived in second-order logic from Hume's principle. It was first proven, informally, by Gottlob Frege in his 1884 Die Grundlagen der Arithmetik and proven more formally in his 1893 Grundgesetze der Arithmetik I. The theorem was re-discovered by Crispin Wright in the early 1980s and has since been the focus of significant work. It is at the core of the philosophy of mathematics known as neo-logicism.
Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.
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.
Logic is the systematic study of valid rules of inference, i.e. the relations that lead to the acceptance of one proposition on the basis of a set of other propositions (premises). More broadly, logic is the analysis and appraisal of arguments.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
