Mixing
Predicate logic: How do you self-check the logical structure of your own arguments?
$begingroup$
In propositional logic, there are truth tables. So you can check if the logical structure of your argument is, not correct per se, but if it's what you intended it to be.
In predicate logic, I have seen no reference to truth tables, nor have I seen any use (literal use) of truth tables when searching for examples where truth tables are used in PL.
It would be nice to check the logical structure of my own arguments, as I will not always have someone to validate my own work. I plan on employing my skills in logic, but I want a sure fire way to ensure that my form is correct :)
logic predicate-logic
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
$endgroup$
add a comment |
$begingroup$
In propositional logic, there are truth tables. So you can check if the logical structure of your argument is, not correct per se, but if it's what you intended it to be.
In predicate logic, I have seen no reference to truth tables, nor have I seen any use (literal use) of truth tables when searching for examples where truth tables are used in PL.
It would be nice to check the logical structure of my own arguments, as I will not always have someone to validate my own work. I plan on employing my skills in logic, but I want a sure fire way to ensure that my form is correct :)
logic predicate-logic
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
$endgroup$
1
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26
add a comment |
$begingroup$
In propositional logic, there are truth tables. So you can check if the logical structure of your argument is, not correct per se, but if it's what you intended it to be.
In predicate logic, I have seen no reference to truth tables, nor have I seen any use (literal use) of truth tables when searching for examples where truth tables are used in PL.
It would be nice to check the logical structure of my own arguments, as I will not always have someone to validate my own work. I plan on employing my skills in logic, but I want a sure fire way to ensure that my form is correct :)
logic predicate-logic
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
$endgroup$
In propositional logic, there are truth tables. So you can check if the logical structure of your argument is, not correct per se, but if it's what you intended it to be.
In predicate logic, I have seen no reference to truth tables, nor have I seen any use (literal use) of truth tables when searching for examples where truth tables are used in PL.
It would be nice to check the logical structure of my own arguments, as I will not always have someone to validate my own work. I plan on employing my skills in logic, but I want a sure fire way to ensure that my form is correct :)
logic predicate-logic
logic predicate-logic
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
asked Mar 3 '16 at 18:52
Jim JamJim Jam
6601721
6601721
1
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26
add a comment |
1
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26
1
1
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).
What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$
Contexts
Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.
For example a case analysis would look like:
$sub{If $A$}{...} \ sub{If $neg A$}{...}$
And reasoning about an arbitrary member of a collection $S$ would look like:
$sub{Given $x in S$}{...}$
Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic the above two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.
Syntax rules
A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
Natural deduction rules
Each inference rule is of the form:
$fitch{text{X}}{text{Y}}$
which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, which is defined to be the context of "X". We will not mention "current context" all the time.
Boolean operations
Take any statements $A,B,C$ (in the current context).
restate: If we prove something we can affirm it again in the same context.
$fitch{A.\...}{A.}$
Note that "$...$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$A.$" must be in the same context (or some subcontext).
In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:
$fitch{A. \ ...}{[A.]}$
⇒sub ⇒restate (We can create a conditional subcontext where $A$ holds.)
$fitch{}{sub{If $A$}{[A.]}}$
$fitch{B. \ ... \ sub{If $A$}{...}}{block{[B.]}}$
⇒intro ⇒elim ("$imp$" internally captures contextual statements.)
$fitch{sub{If $A$}{... \ B. \ ...} \ ...}{[A imp B.]}$
$fitch{A imp B. \ A.}{B.}$
∧intro ∧elim
$fitch{A. \ B.}{A land B.}$
$fitch{A land B.}{[A.] \ [B.]}$
∨intro ∨elim
$fitch{A.}{[A lor B.] \ [B lor A.]}$
$fitch{A lor B. \ A imp C. \ B imp C.}{C.}$
¬intro ¬elim ¬¬elim
$fitch{A imp bot.}{neg A.}$
$fitch{A. \ neg A.}{bot.}$
$fitch{neg neg A.}{A.}$
Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:
$fitch{neg A imp bot.}{A.}$
which corresponds to how one would attempt to prove $A$ by contradiction, namely to show that assuming $neg A$ implies a falsehood.
⇔intro ⇔elim
$fitch{A imp B. \ B imp A.}{A eq B.}$
$fitch{A eq B.}{[A imp B.] \ [B imp A.]}$
Quantifiers and equality
I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.
Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.
Fresh variable: A variable that does not appear in any previous statement.
Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.
And we need at least one type over which we can quantify, which is provided by the following rule.
universe: $obj$ is a type, which includes all objects.
$fitch{}{[E in obj.]}$
Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.
∀sub ∀restate (We can create a subcontext in which $x$ is of type $S$.)
$fitch{}{sub{Given $x in S$}{[x in S.]}}$
$fitch{A. \ ... \ sub{Given $x in S$}{...}}{block{[A.]}}$ ($x$ must not appear in $A$)
∀intro ∀elim
$fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
$fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)
∃intro ∃elim
$fitch{E in S. \ ... \ P(E). \ ...}{exists x in S ( P(x) ).}$
$fitch{exists x in S ( P(x) ).}{text{Let $y in S$ such that $P(y)$}. \ [y in S.] \ [P(y).]}$ (where $y$ is a fresh variable)
=intro =elim
$fitch{}{[E=E.]}$
$fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)
Variable renaming
Finally, the following rules for variable renaming are redundant, but would significantly shorten proofs.
∀rename ∃rename
$fitch{forall x in S ( P(x) ).}{[forall y in S ( P(y) ).]}$
$fitch{exists x in S ( P(x) ).}{[exists y in S ( P(y) ).]}$
(where $y$ is an unused variable that does not appear in $P$)
Short-forms
For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".
Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in S ( P(y) imp x=y ) )$".
Example
Here is an example, where $S,T$ are any types and $P$ is any property with two parameters.
First with all lines shown:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
$exists x in S ( forall y in T ( P(x,y) ) )$. [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
$a in S$. [∃elim]
$forall y in T ( P(a,y) )$. [∃elim]
$forall z in T ( P(a,z) )$. [∀rename]
Given $y in T$: [∀sub]
$y in T$. [∀sub]
$forall z in T ( P(a,z) )$. [∀restate]
$y in T$. [restate]
$P(a,y)$. [∀elim]
$a in S$. [∀restate]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
Finally with all lines in square-brackets removed:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
Given $y in T$: [∀sub]
$P(a,y)$. [∀elim]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
This final proof is much cleaner yet still easily computer-verifiable.
Notes
The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.
Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$exists x forall x ( x=x )$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.
Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $x$ does not appear in $S,P$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$x∈{y:y∈S∧y∈T}$" and "$x∈U$", it will not be sensible to allow writing "$∃y∈U ( y∈{y:y∈S∧y∈T} )$". Similarly, if we have written "$x={y:P(y)}$" and "$∃y∈U ( Q(x,y) )$", we do not want to allow writing "$∃y∈U ( Q({y:P(y)},y) )$".
To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.
Peano Arithmetic
Add the type $nn$ and the symbols of PA, namely the constant-symbols $0,1$ and the $2$-input function-symbols $+,·$ and the $2$-input predicate-symbol $<$.
Add the axioms of PA$^-$, adapted from here:
$forall x,y in nn ( x+y in nn )$.
$forall x,y in nn ( x·y in nn )$.
$forall x,y in nn ( x+y=y+x )$.
$forall x,y in nn ( x·y=y·x )$.
$forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.
$forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.
$forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.
$forall x in nn ( x+0=x )$.
$forall x in nn ( x·1=x )$.
$forall x in nn ( neg x<x )$.
$forall x,y in nn ( x<y lor y<x lor x=y )$.
$forall x,y,z in nn ( x<y land y<z imp x<z )$.
$forall x,y,z in nn ( x<y imp x+z<y+z )$.
$forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.
$forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.
$0<1$.
$forall x in nn ( 0=x lor 1=x lor 1<x )$.
Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:
$P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in nn ( P(k) )$.
Set Theory
Add the type $set$ and the rule that every member of $set$ is also a type.
Add the unary function-symbols $pow,bigcup$, the binary function-symbols $×,FN$, and the constant-symbol $none$. We reuse the binary predicate-symbol $in$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:
- If $E,F in obj$, then $(E,F) in obj$ and ${E,F} in set$.
- If $S,T in set$, then $S×T in set$ and $FN(S,T) in set$ and $pow(S) in set$.
- If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.
- If $forall x in S ( x in set )$, then $bigcup(S) in set$.
Add the following axioms:
extensionality: $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
empty-set: $forall x in obj ( neg x in none ).$
power-set: $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
pair: $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
ordered-pair: $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
product-type: $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
function-type: $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
function-application: $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
union: $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
choice: $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
Add the following rules:
type-notation
Take (in the current context) any property $P$ and object expression $E$ and unused variable $x$.
Then ${ x : P(x) }$ is a type and its membership is governed by:
$fitch{}{E in { x : P(x) } eq P(E).}$. ($x$ must not appear in $E$ or $P$)
comprehension
Take any property $P$ and unused variable $x$.
$fitch{S in set.}{{ x : x in S land P(x) } in set.}$. ($x$ must not appear in $S$ or $P$)
collection
Take any $2$-parameter property $P$ and unused variables $x,y$.
$fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in S ( P(x,y) ) } in set.}$ ($x,y$ must not appear in $S$ or $P$)
induction
Take any property $P$ with $1$ parameter from $nn$.
$fitch{P(0). \ forall k in nn ( P(k) imp P(k+1) ).}{forall k in nn ( P(k) ).}$ ($k$ must not appear in $P$)
The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $P$ can involve set operations and quantification over sets.
function-notation
This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).
Take any set $S$ and any object expression $E$ with $1$ parameter from $S$, and unused variable $x$.
Then $( S x mapsto E(x) )$ is an object and its behaviour is governed by:
$fitch{forall x in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in S ( f(x) = E(x) ).}$
Foundational system
Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $nn$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
$endgroup$
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f1681857%2fpredicate-logic-how-do-you-self-check-the-logical-structure-of-your-own-argumen%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).
What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$
Contexts
Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.
For example a case analysis would look like:
$sub{If $A$}{...} \ sub{If $neg A$}{...}$
And reasoning about an arbitrary member of a collection $S$ would look like:
$sub{Given $x in S$}{...}$
Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic the above two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.
Syntax rules
A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
Natural deduction rules
Each inference rule is of the form:
$fitch{text{X}}{text{Y}}$
which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, which is defined to be the context of "X". We will not mention "current context" all the time.
Boolean operations
Take any statements $A,B,C$ (in the current context).
restate: If we prove something we can affirm it again in the same context.
$fitch{A.\...}{A.}$
Note that "$...$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$A.$" must be in the same context (or some subcontext).
In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:
$fitch{A. \ ...}{[A.]}$
⇒sub ⇒restate (We can create a conditional subcontext where $A$ holds.)
$fitch{}{sub{If $A$}{[A.]}}$
$fitch{B. \ ... \ sub{If $A$}{...}}{block{[B.]}}$
⇒intro ⇒elim ("$imp$" internally captures contextual statements.)
$fitch{sub{If $A$}{... \ B. \ ...} \ ...}{[A imp B.]}$
$fitch{A imp B. \ A.}{B.}$
∧intro ∧elim
$fitch{A. \ B.}{A land B.}$
$fitch{A land B.}{[A.] \ [B.]}$
∨intro ∨elim
$fitch{A.}{[A lor B.] \ [B lor A.]}$
$fitch{A lor B. \ A imp C. \ B imp C.}{C.}$
¬intro ¬elim ¬¬elim
$fitch{A imp bot.}{neg A.}$
$fitch{A. \ neg A.}{bot.}$
$fitch{neg neg A.}{A.}$
Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:
$fitch{neg A imp bot.}{A.}$
which corresponds to how one would attempt to prove $A$ by contradiction, namely to show that assuming $neg A$ implies a falsehood.
⇔intro ⇔elim
$fitch{A imp B. \ B imp A.}{A eq B.}$
$fitch{A eq B.}{[A imp B.] \ [B imp A.]}$
Quantifiers and equality
I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.
Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.
Fresh variable: A variable that does not appear in any previous statement.
Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.
And we need at least one type over which we can quantify, which is provided by the following rule.
universe: $obj$ is a type, which includes all objects.
$fitch{}{[E in obj.]}$
Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.
∀sub ∀restate (We can create a subcontext in which $x$ is of type $S$.)
$fitch{}{sub{Given $x in S$}{[x in S.]}}$
$fitch{A. \ ... \ sub{Given $x in S$}{...}}{block{[A.]}}$ ($x$ must not appear in $A$)
∀intro ∀elim
$fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
$fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)
∃intro ∃elim
$fitch{E in S. \ ... \ P(E). \ ...}{exists x in S ( P(x) ).}$
$fitch{exists x in S ( P(x) ).}{text{Let $y in S$ such that $P(y)$}. \ [y in S.] \ [P(y).]}$ (where $y$ is a fresh variable)
=intro =elim
$fitch{}{[E=E.]}$
$fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)
Variable renaming
Finally, the following rules for variable renaming are redundant, but would significantly shorten proofs.
∀rename ∃rename
$fitch{forall x in S ( P(x) ).}{[forall y in S ( P(y) ).]}$
$fitch{exists x in S ( P(x) ).}{[exists y in S ( P(y) ).]}$
(where $y$ is an unused variable that does not appear in $P$)
Short-forms
For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".
Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in S ( P(y) imp x=y ) )$".
Example
Here is an example, where $S,T$ are any types and $P$ is any property with two parameters.
First with all lines shown:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
$exists x in S ( forall y in T ( P(x,y) ) )$. [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
$a in S$. [∃elim]
$forall y in T ( P(a,y) )$. [∃elim]
$forall z in T ( P(a,z) )$. [∀rename]
Given $y in T$: [∀sub]
$y in T$. [∀sub]
$forall z in T ( P(a,z) )$. [∀restate]
$y in T$. [restate]
$P(a,y)$. [∀elim]
$a in S$. [∀restate]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
Finally with all lines in square-brackets removed:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
Given $y in T$: [∀sub]
$P(a,y)$. [∀elim]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
This final proof is much cleaner yet still easily computer-verifiable.
Notes
The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.
Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$exists x forall x ( x=x )$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.
Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $x$ does not appear in $S,P$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$x∈{y:y∈S∧y∈T}$" and "$x∈U$", it will not be sensible to allow writing "$∃y∈U ( y∈{y:y∈S∧y∈T} )$". Similarly, if we have written "$x={y:P(y)}$" and "$∃y∈U ( Q(x,y) )$", we do not want to allow writing "$∃y∈U ( Q({y:P(y)},y) )$".
To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.
Peano Arithmetic
Add the type $nn$ and the symbols of PA, namely the constant-symbols $0,1$ and the $2$-input function-symbols $+,·$ and the $2$-input predicate-symbol $<$.
Add the axioms of PA$^-$, adapted from here:
$forall x,y in nn ( x+y in nn )$.
$forall x,y in nn ( x·y in nn )$.
$forall x,y in nn ( x+y=y+x )$.
$forall x,y in nn ( x·y=y·x )$.
$forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.
$forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.
$forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.
$forall x in nn ( x+0=x )$.
$forall x in nn ( x·1=x )$.
$forall x in nn ( neg x<x )$.
$forall x,y in nn ( x<y lor y<x lor x=y )$.
$forall x,y,z in nn ( x<y land y<z imp x<z )$.
$forall x,y,z in nn ( x<y imp x+z<y+z )$.
$forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.
$forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.
$0<1$.
$forall x in nn ( 0=x lor 1=x lor 1<x )$.
Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:
$P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in nn ( P(k) )$.
Set Theory
Add the type $set$ and the rule that every member of $set$ is also a type.
Add the unary function-symbols $pow,bigcup$, the binary function-symbols $×,FN$, and the constant-symbol $none$. We reuse the binary predicate-symbol $in$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:
- If $E,F in obj$, then $(E,F) in obj$ and ${E,F} in set$.
- If $S,T in set$, then $S×T in set$ and $FN(S,T) in set$ and $pow(S) in set$.
- If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.
- If $forall x in S ( x in set )$, then $bigcup(S) in set$.
Add the following axioms:
extensionality: $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
empty-set: $forall x in obj ( neg x in none ).$
power-set: $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
pair: $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
ordered-pair: $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
product-type: $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
function-type: $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
function-application: $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
union: $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
choice: $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
Add the following rules:
type-notation
Take (in the current context) any property $P$ and object expression $E$ and unused variable $x$.
Then ${ x : P(x) }$ is a type and its membership is governed by:
$fitch{}{E in { x : P(x) } eq P(E).}$. ($x$ must not appear in $E$ or $P$)
comprehension
Take any property $P$ and unused variable $x$.
$fitch{S in set.}{{ x : x in S land P(x) } in set.}$. ($x$ must not appear in $S$ or $P$)
collection
Take any $2$-parameter property $P$ and unused variables $x,y$.
$fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in S ( P(x,y) ) } in set.}$ ($x,y$ must not appear in $S$ or $P$)
induction
Take any property $P$ with $1$ parameter from $nn$.
$fitch{P(0). \ forall k in nn ( P(k) imp P(k+1) ).}{forall k in nn ( P(k) ).}$ ($k$ must not appear in $P$)
The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $P$ can involve set operations and quantification over sets.
function-notation
This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).
Take any set $S$ and any object expression $E$ with $1$ parameter from $S$, and unused variable $x$.
Then $( S x mapsto E(x) )$ is an object and its behaviour is governed by:
$fitch{forall x in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in S ( f(x) = E(x) ).}$
Foundational system
Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $nn$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
$endgroup$
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
add a comment |
$begingroup$
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).
What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$
Contexts
Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.
For example a case analysis would look like:
$sub{If $A$}{...} \ sub{If $neg A$}{...}$
And reasoning about an arbitrary member of a collection $S$ would look like:
$sub{Given $x in S$}{...}$
Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic the above two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.
Syntax rules
A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
Natural deduction rules
Each inference rule is of the form:
$fitch{text{X}}{text{Y}}$
which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, which is defined to be the context of "X". We will not mention "current context" all the time.
Boolean operations
Take any statements $A,B,C$ (in the current context).
restate: If we prove something we can affirm it again in the same context.
$fitch{A.\...}{A.}$
Note that "$...$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$A.$" must be in the same context (or some subcontext).
In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:
$fitch{A. \ ...}{[A.]}$
⇒sub ⇒restate (We can create a conditional subcontext where $A$ holds.)
$fitch{}{sub{If $A$}{[A.]}}$
$fitch{B. \ ... \ sub{If $A$}{...}}{block{[B.]}}$
⇒intro ⇒elim ("$imp$" internally captures contextual statements.)
$fitch{sub{If $A$}{... \ B. \ ...} \ ...}{[A imp B.]}$
$fitch{A imp B. \ A.}{B.}$
∧intro ∧elim
$fitch{A. \ B.}{A land B.}$
$fitch{A land B.}{[A.] \ [B.]}$
∨intro ∨elim
$fitch{A.}{[A lor B.] \ [B lor A.]}$
$fitch{A lor B. \ A imp C. \ B imp C.}{C.}$
¬intro ¬elim ¬¬elim
$fitch{A imp bot.}{neg A.}$
$fitch{A. \ neg A.}{bot.}$
$fitch{neg neg A.}{A.}$
Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:
$fitch{neg A imp bot.}{A.}$
which corresponds to how one would attempt to prove $A$ by contradiction, namely to show that assuming $neg A$ implies a falsehood.
⇔intro ⇔elim
$fitch{A imp B. \ B imp A.}{A eq B.}$
$fitch{A eq B.}{[A imp B.] \ [B imp A.]}$
Quantifiers and equality
I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.
Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.
Fresh variable: A variable that does not appear in any previous statement.
Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.
And we need at least one type over which we can quantify, which is provided by the following rule.
universe: $obj$ is a type, which includes all objects.
$fitch{}{[E in obj.]}$
Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.
∀sub ∀restate (We can create a subcontext in which $x$ is of type $S$.)
$fitch{}{sub{Given $x in S$}{[x in S.]}}$
$fitch{A. \ ... \ sub{Given $x in S$}{...}}{block{[A.]}}$ ($x$ must not appear in $A$)
∀intro ∀elim
$fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
$fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)
∃intro ∃elim
$fitch{E in S. \ ... \ P(E). \ ...}{exists x in S ( P(x) ).}$
$fitch{exists x in S ( P(x) ).}{text{Let $y in S$ such that $P(y)$}. \ [y in S.] \ [P(y).]}$ (where $y$ is a fresh variable)
=intro =elim
$fitch{}{[E=E.]}$
$fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)
Variable renaming
Finally, the following rules for variable renaming are redundant, but would significantly shorten proofs.
∀rename ∃rename
$fitch{forall x in S ( P(x) ).}{[forall y in S ( P(y) ).]}$
$fitch{exists x in S ( P(x) ).}{[exists y in S ( P(y) ).]}$
(where $y$ is an unused variable that does not appear in $P$)
Short-forms
For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".
Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in S ( P(y) imp x=y ) )$".
Example
Here is an example, where $S,T$ are any types and $P$ is any property with two parameters.
First with all lines shown:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
$exists x in S ( forall y in T ( P(x,y) ) )$. [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
$a in S$. [∃elim]
$forall y in T ( P(a,y) )$. [∃elim]
$forall z in T ( P(a,z) )$. [∀rename]
Given $y in T$: [∀sub]
$y in T$. [∀sub]
$forall z in T ( P(a,z) )$. [∀restate]
$y in T$. [restate]
$P(a,y)$. [∀elim]
$a in S$. [∀restate]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
Finally with all lines in square-brackets removed:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
Given $y in T$: [∀sub]
$P(a,y)$. [∀elim]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
This final proof is much cleaner yet still easily computer-verifiable.
Notes
The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.
Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$exists x forall x ( x=x )$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.
Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $x$ does not appear in $S,P$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$x∈{y:y∈S∧y∈T}$" and "$x∈U$", it will not be sensible to allow writing "$∃y∈U ( y∈{y:y∈S∧y∈T} )$". Similarly, if we have written "$x={y:P(y)}$" and "$∃y∈U ( Q(x,y) )$", we do not want to allow writing "$∃y∈U ( Q({y:P(y)},y) )$".
To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.
Peano Arithmetic
Add the type $nn$ and the symbols of PA, namely the constant-symbols $0,1$ and the $2$-input function-symbols $+,·$ and the $2$-input predicate-symbol $<$.
Add the axioms of PA$^-$, adapted from here:
$forall x,y in nn ( x+y in nn )$.
$forall x,y in nn ( x·y in nn )$.
$forall x,y in nn ( x+y=y+x )$.
$forall x,y in nn ( x·y=y·x )$.
$forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.
$forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.
$forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.
$forall x in nn ( x+0=x )$.
$forall x in nn ( x·1=x )$.
$forall x in nn ( neg x<x )$.
$forall x,y in nn ( x<y lor y<x lor x=y )$.
$forall x,y,z in nn ( x<y land y<z imp x<z )$.
$forall x,y,z in nn ( x<y imp x+z<y+z )$.
$forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.
$forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.
$0<1$.
$forall x in nn ( 0=x lor 1=x lor 1<x )$.
Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:
$P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in nn ( P(k) )$.
Set Theory
Add the type $set$ and the rule that every member of $set$ is also a type.
Add the unary function-symbols $pow,bigcup$, the binary function-symbols $×,FN$, and the constant-symbol $none$. We reuse the binary predicate-symbol $in$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:
- If $E,F in obj$, then $(E,F) in obj$ and ${E,F} in set$.
- If $S,T in set$, then $S×T in set$ and $FN(S,T) in set$ and $pow(S) in set$.
- If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.
- If $forall x in S ( x in set )$, then $bigcup(S) in set$.
Add the following axioms:
extensionality: $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
empty-set: $forall x in obj ( neg x in none ).$
power-set: $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
pair: $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
ordered-pair: $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
product-type: $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
function-type: $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
function-application: $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
union: $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
choice: $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
Add the following rules:
type-notation
Take (in the current context) any property $P$ and object expression $E$ and unused variable $x$.
Then ${ x : P(x) }$ is a type and its membership is governed by:
$fitch{}{E in { x : P(x) } eq P(E).}$. ($x$ must not appear in $E$ or $P$)
comprehension
Take any property $P$ and unused variable $x$.
$fitch{S in set.}{{ x : x in S land P(x) } in set.}$. ($x$ must not appear in $S$ or $P$)
collection
Take any $2$-parameter property $P$ and unused variables $x,y$.
$fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in S ( P(x,y) ) } in set.}$ ($x,y$ must not appear in $S$ or $P$)
induction
Take any property $P$ with $1$ parameter from $nn$.
$fitch{P(0). \ forall k in nn ( P(k) imp P(k+1) ).}{forall k in nn ( P(k) ).}$ ($k$ must not appear in $P$)
The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $P$ can involve set operations and quantification over sets.
function-notation
This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).
Take any set $S$ and any object expression $E$ with $1$ parameter from $S$, and unused variable $x$.
Then $( S x mapsto E(x) )$ is an object and its behaviour is governed by:
$fitch{forall x in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in S ( f(x) = E(x) ).}$
Foundational system
Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $nn$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
$endgroup$
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
add a comment |
$begingroup$
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).
What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$
Contexts
Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.
For example a case analysis would look like:
$sub{If $A$}{...} \ sub{If $neg A$}{...}$
And reasoning about an arbitrary member of a collection $S$ would look like:
$sub{Given $x in S$}{...}$
Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic the above two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.
Syntax rules
A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
Natural deduction rules
Each inference rule is of the form:
$fitch{text{X}}{text{Y}}$
which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, which is defined to be the context of "X". We will not mention "current context" all the time.
Boolean operations
Take any statements $A,B,C$ (in the current context).
restate: If we prove something we can affirm it again in the same context.
$fitch{A.\...}{A.}$
Note that "$...$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$A.$" must be in the same context (or some subcontext).
In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:
$fitch{A. \ ...}{[A.]}$
⇒sub ⇒restate (We can create a conditional subcontext where $A$ holds.)
$fitch{}{sub{If $A$}{[A.]}}$
$fitch{B. \ ... \ sub{If $A$}{...}}{block{[B.]}}$
⇒intro ⇒elim ("$imp$" internally captures contextual statements.)
$fitch{sub{If $A$}{... \ B. \ ...} \ ...}{[A imp B.]}$
$fitch{A imp B. \ A.}{B.}$
∧intro ∧elim
$fitch{A. \ B.}{A land B.}$
$fitch{A land B.}{[A.] \ [B.]}$
∨intro ∨elim
$fitch{A.}{[A lor B.] \ [B lor A.]}$
$fitch{A lor B. \ A imp C. \ B imp C.}{C.}$
¬intro ¬elim ¬¬elim
$fitch{A imp bot.}{neg A.}$
$fitch{A. \ neg A.}{bot.}$
$fitch{neg neg A.}{A.}$
Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:
$fitch{neg A imp bot.}{A.}$
which corresponds to how one would attempt to prove $A$ by contradiction, namely to show that assuming $neg A$ implies a falsehood.
⇔intro ⇔elim
$fitch{A imp B. \ B imp A.}{A eq B.}$
$fitch{A eq B.}{[A imp B.] \ [B imp A.]}$
Quantifiers and equality
I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.
Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.
Fresh variable: A variable that does not appear in any previous statement.
Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.
And we need at least one type over which we can quantify, which is provided by the following rule.
universe: $obj$ is a type, which includes all objects.
$fitch{}{[E in obj.]}$
Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.
∀sub ∀restate (We can create a subcontext in which $x$ is of type $S$.)
$fitch{}{sub{Given $x in S$}{[x in S.]}}$
$fitch{A. \ ... \ sub{Given $x in S$}{...}}{block{[A.]}}$ ($x$ must not appear in $A$)
∀intro ∀elim
$fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
$fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)
∃intro ∃elim
$fitch{E in S. \ ... \ P(E). \ ...}{exists x in S ( P(x) ).}$
$fitch{exists x in S ( P(x) ).}{text{Let $y in S$ such that $P(y)$}. \ [y in S.] \ [P(y).]}$ (where $y$ is a fresh variable)
=intro =elim
$fitch{}{[E=E.]}$
$fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)
Variable renaming
Finally, the following rules for variable renaming are redundant, but would significantly shorten proofs.
∀rename ∃rename
$fitch{forall x in S ( P(x) ).}{[forall y in S ( P(y) ).]}$
$fitch{exists x in S ( P(x) ).}{[exists y in S ( P(y) ).]}$
(where $y$ is an unused variable that does not appear in $P$)
Short-forms
For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".
Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in S ( P(y) imp x=y ) )$".
Example
Here is an example, where $S,T$ are any types and $P$ is any property with two parameters.
First with all lines shown:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
$exists x in S ( forall y in T ( P(x,y) ) )$. [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
$a in S$. [∃elim]
$forall y in T ( P(a,y) )$. [∃elim]
$forall z in T ( P(a,z) )$. [∀rename]
Given $y in T$: [∀sub]
$y in T$. [∀sub]
$forall z in T ( P(a,z) )$. [∀restate]
$y in T$. [restate]
$P(a,y)$. [∀elim]
$a in S$. [∀restate]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
Finally with all lines in square-brackets removed:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
Given $y in T$: [∀sub]
$P(a,y)$. [∀elim]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
This final proof is much cleaner yet still easily computer-verifiable.
Notes
The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.
Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$exists x forall x ( x=x )$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.
Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $x$ does not appear in $S,P$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$x∈{y:y∈S∧y∈T}$" and "$x∈U$", it will not be sensible to allow writing "$∃y∈U ( y∈{y:y∈S∧y∈T} )$". Similarly, if we have written "$x={y:P(y)}$" and "$∃y∈U ( Q(x,y) )$", we do not want to allow writing "$∃y∈U ( Q({y:P(y)},y) )$".
To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.
Peano Arithmetic
Add the type $nn$ and the symbols of PA, namely the constant-symbols $0,1$ and the $2$-input function-symbols $+,·$ and the $2$-input predicate-symbol $<$.
Add the axioms of PA$^-$, adapted from here:
$forall x,y in nn ( x+y in nn )$.
$forall x,y in nn ( x·y in nn )$.
$forall x,y in nn ( x+y=y+x )$.
$forall x,y in nn ( x·y=y·x )$.
$forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.
$forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.
$forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.
$forall x in nn ( x+0=x )$.
$forall x in nn ( x·1=x )$.
$forall x in nn ( neg x<x )$.
$forall x,y in nn ( x<y lor y<x lor x=y )$.
$forall x,y,z in nn ( x<y land y<z imp x<z )$.
$forall x,y,z in nn ( x<y imp x+z<y+z )$.
$forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.
$forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.
$0<1$.
$forall x in nn ( 0=x lor 1=x lor 1<x )$.
Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:
$P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in nn ( P(k) )$.
Set Theory
Add the type $set$ and the rule that every member of $set$ is also a type.
Add the unary function-symbols $pow,bigcup$, the binary function-symbols $×,FN$, and the constant-symbol $none$. We reuse the binary predicate-symbol $in$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:
- If $E,F in obj$, then $(E,F) in obj$ and ${E,F} in set$.
- If $S,T in set$, then $S×T in set$ and $FN(S,T) in set$ and $pow(S) in set$.
- If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.
- If $forall x in S ( x in set )$, then $bigcup(S) in set$.
Add the following axioms:
extensionality: $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
empty-set: $forall x in obj ( neg x in none ).$
power-set: $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
pair: $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
ordered-pair: $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
product-type: $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
function-type: $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
function-application: $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
union: $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
choice: $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
Add the following rules:
type-notation
Take (in the current context) any property $P$ and object expression $E$ and unused variable $x$.
Then ${ x : P(x) }$ is a type and its membership is governed by:
$fitch{}{E in { x : P(x) } eq P(E).}$. ($x$ must not appear in $E$ or $P$)
comprehension
Take any property $P$ and unused variable $x$.
$fitch{S in set.}{{ x : x in S land P(x) } in set.}$. ($x$ must not appear in $S$ or $P$)
collection
Take any $2$-parameter property $P$ and unused variables $x,y$.
$fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in S ( P(x,y) ) } in set.}$ ($x,y$ must not appear in $S$ or $P$)
induction
Take any property $P$ with $1$ parameter from $nn$.
$fitch{P(0). \ forall k in nn ( P(k) imp P(k+1) ).}{forall k in nn ( P(k) ).}$ ($k$ must not appear in $P$)
The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $P$ can involve set operations and quantification over sets.
function-notation
This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).
Take any set $S$ and any object expression $E$ with $1$ parameter from $S$, and unused variable $x$.
Then $( S x mapsto E(x) )$ is an object and its behaviour is governed by:
$fitch{forall x in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in S ( f(x) = E(x) ).}$
Foundational system
Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $nn$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
$endgroup$
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preserving. If you choose carefully enough, you can make it so that the rules are not just truth-preserving but also allow you to deduce every (well-formed) statement that is necessarily true (in all situations).
What you are probably looking for (namely a practical way to rigorously check the logical validity of your arguments) is natural deduction. There are many different styles, the most intuitive type being Fitch-style, which mark subcontexts using indentation or some related visual demarcation. The following system uses indentation and follows the intuition most closely in my opinion.
$
defblock#1{begin{array}{ll} &{#1}end{array}}
deffitch#1#2{begin{array}{|l}#1\hline#2end{array}}
defsub#1#2{text{#1}:\block{#2}}
defimp{Rightarrow}
defeq{Leftrightarrow}
defnn{mathbb{N}}
defnone{varnothing}
defpow{mathcal{P}}
$
Contexts
Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.
For example a case analysis would look like:
$sub{If $A$}{...} \ sub{If $neg A$}{...}$
And reasoning about an arbitrary member of a collection $S$ would look like:
$sub{Given $x in S$}{...}$
Note that what is stated in some context may be invalid in other contexts. Once you understand the principle behind contexts and the indentation, the following rules are very natural. Also note that for first-order logic the above two kinds of context headers (for conditional subcontexts and universal subcontexts respectively) are the only kinds needed.
Syntax rules
A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
Natural deduction rules
Each inference rule is of the form:
$fitch{text{X}}{text{Y}}$
which means that if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation. Each application of an inference rule is also tied to the current context, which is defined to be the context of "X". We will not mention "current context" all the time.
Boolean operations
Take any statements $A,B,C$ (in the current context).
restate: If we prove something we can affirm it again in the same context.
$fitch{A.\...}{A.}$
Note that "$...$" denote any number of lines that are at least at the depicted indentation level. In the above rule, this means that all the lines written since the earlier writing of "$A.$" must be in the same context (or some subcontext).
In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows:
$fitch{A. \ ...}{[A.]}$
⇒sub ⇒restate (We can create a conditional subcontext where $A$ holds.)
$fitch{}{sub{If $A$}{[A.]}}$
$fitch{B. \ ... \ sub{If $A$}{...}}{block{[B.]}}$
⇒intro ⇒elim ("$imp$" internally captures contextual statements.)
$fitch{sub{If $A$}{... \ B. \ ...} \ ...}{[A imp B.]}$
$fitch{A imp B. \ A.}{B.}$
∧intro ∧elim
$fitch{A. \ B.}{A land B.}$
$fitch{A land B.}{[A.] \ [B.]}$
∨intro ∨elim
$fitch{A.}{[A lor B.] \ [B lor A.]}$
$fitch{A lor B. \ A imp C. \ B imp C.}{C.}$
¬intro ¬elim ¬¬elim
$fitch{A imp bot.}{neg A.}$
$fitch{A. \ neg A.}{bot.}$
$fitch{neg neg A.}{A.}$
Note that by using ¬intro and ¬¬elim we can get the following additional inference rule:
$fitch{neg A imp bot.}{A.}$
which corresponds to how one would attempt to prove $A$ by contradiction, namely to show that assuming $neg A$ implies a falsehood.
⇔intro ⇔elim
$fitch{A imp B. \ B imp A.}{A eq B.}$
$fitch{A eq B.}{[A imp B.] \ [B imp A.]}$
Quantifiers and equality
I show the rules for restricted quantifiers because usually we think in terms of them. First we need some definitions.
Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts.
Fresh variable: A variable that does not appear in any previous statement.
Object expression: An expression that refers to an object. In classical first-order logic, the object expressions are simply the well-formed terms (whose free variables are each declared in the header of some containing ∀-subcontext). In the following rules $E,F$ (if involved) can be any object expressions.
And we need at least one type over which we can quantify, which is provided by the following rule.
universe: $obj$ is a type, which includes all objects.
$fitch{}{[E in obj.]}$
Now take any type $S$ and a property $P$ and an unused variable $x$ that does not appear in $S$ or $P$. By $P$ being a property we mean that $P(x)$ is a statement about $x$.
∀sub ∀restate (We can create a subcontext in which $x$ is of type $S$.)
$fitch{}{sub{Given $x in S$}{[x in S.]}}$
$fitch{A. \ ... \ sub{Given $x in S$}{...}}{block{[A.]}}$ ($x$ must not appear in $A$)
∀intro ∀elim
$fitch{sub{Given $x in S$}{... \ P(x). \ ...} \ ...}{forall x in S ( P(x) ).}$
$fitch{forall x in S ( P(x) ). \ ... \ E in S. \ ...}{P(E).}$ (unused variables appearing in $P$ must not appear in $E$)
∃intro ∃elim
$fitch{E in S. \ ... \ P(E). \ ...}{exists x in S ( P(x) ).}$
$fitch{exists x in S ( P(x) ).}{text{Let $y in S$ such that $P(y)$}. \ [y in S.] \ [P(y).]}$ (where $y$ is a fresh variable)
=intro =elim
$fitch{}{[E=E.]}$
$fitch{E=F. \ P(E).}{P(F).}$ (unused variables appearing in $P$ must not appear in $F$)
Variable renaming
Finally, the following rules for variable renaming are redundant, but would significantly shorten proofs.
∀rename ∃rename
$fitch{forall x in S ( P(x) ).}{[forall y in S ( P(y) ).]}$
$fitch{exists x in S ( P(x) ).}{[exists y in S ( P(y) ).]}$
(where $y$ is an unused variable that does not appear in $P$)
Short-forms
For convenience we also write "$forall x,y in S ( P(x,y) )$" as short-form for "$forall x in S ( forall y in S ( P(x,y) ) )$", and similarly for more variables and for "$exists$".
Additionally, "$exists! x in S ( P(x) )$" is short-form for "$exists x in S ( P(x) land forall y in S ( P(y) imp x=y ) )$".
Example
Here is an example, where $S,T$ are any types and $P$ is any property with two parameters.
First with all lines shown:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
$exists x in S ( forall y in T ( P(x,y) ) )$. [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
$a in S$. [∃elim]
$forall y in T ( P(a,y) )$. [∃elim]
$forall z in T ( P(a,z) )$. [∀rename]
Given $y in T$: [∀sub]
$y in T$. [∀sub]
$forall z in T ( P(a,z) )$. [∀restate]
$y in T$. [restate]
$P(a,y)$. [∀elim]
$a in S$. [∀restate]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
Finally with all lines in square-brackets removed:
If $exists x in S ( forall y in T ( P(x,y) ) )$: [⇒sub]
Let $a in S$ such that $forall y in T ( P(a,y) )$. [∃elim]
Given $y in T$: [∀sub]
$P(a,y)$. [∀elim]
$exists x in S ( P(x,y) )$. [∃intro]
$forall y in T ( exists x in S ( P(x,y) ) )$. [∀intro]
$exists x in S ( forall y in T ( P(x,y) ) ) imp forall y in T ( exists x in S ( P(x,y) ) )$. [⇒intro]
This final proof is much cleaner yet still easily computer-verifiable.
Notes
The above rules avoid the usual trouble that most other systems have, where variables used for witnesses of existential statements must be distinguished from variables used for arbitrary objects. The reason is that every variable here is either specified by a ∀-subcontext or by a "let"-statement; in other words there are no free variables. The fact that every variable is bound is strongly related to the fact that this system allows an empty universe, if there are no other axioms.
Also, every variable is specified by a unique header or "let"-statement in the current context; in other words there is no variable shadowing. This is by design, and in actual mathematical practice we also abide by this, though most other formal systems do not. As a consequence, sentences such as "$exists x forall x ( x=x )$." simply cannot be written down in this system. If you wish to permit such kind of terrible sentences, you would have to modify the rules appropriately, but it will most probably cause a headache.
Finally, there were some subtle technical decisions. For the quantifier rules, the reason I required that $x$ does not appear in $S,P$ is that, if we later on include rules for specifying types, we would usually have variable names in its syntax, which would cause problems. For example, if we have written in the current context "$x∈{y:y∈S∧y∈T}$" and "$x∈U$", it will not be sensible to allow writing "$∃y∈U ( y∈{y:y∈S∧y∈T} )$". Similarly, if we have written "$x={y:P(y)}$" and "$∃y∈U ( Q(x,y) )$", we do not want to allow writing "$∃y∈U ( Q({y:P(y)},y) )$".
To illustrate the flexibility of this system, I will express both Peano Arithmetic and Set Theory as extra rules that can be simply added to the system.
Peano Arithmetic
Add the type $nn$ and the symbols of PA, namely the constant-symbols $0,1$ and the $2$-input function-symbols $+,·$ and the $2$-input predicate-symbol $<$.
Add the axioms of PA$^-$, adapted from here:
$forall x,y in nn ( x+y in nn )$.
$forall x,y in nn ( x·y in nn )$.
$forall x,y in nn ( x+y=y+x )$.
$forall x,y in nn ( x·y=y·x )$.
$forall x,y,z in nn ( x+(y+z)=(x+y)+z )$.
$forall x,y,z in nn ( x·(y·z)=(x·y)·z )$.
$forall x,y,z in nn ( x·(y+z)=x·z+y·z )$.
$forall x in nn ( x+0=x )$.
$forall x in nn ( x·1=x )$.
$forall x in nn ( neg x<x )$.
$forall x,y in nn ( x<y lor y<x lor x=y )$.
$forall x,y,z in nn ( x<y land y<z imp x<z )$.
$forall x,y,z in nn ( x<y imp x+z<y+z )$.
$forall x,y,z in nn ( x<y land 0<z imp x·z<y·z )$.
$forall x,y in nn ( x<y imp exists z in nn ( x+z=y ) )$.
$0<1$.
$forall x in nn ( 0=x lor 1=x lor 1<x )$.
Add the induction axioms, namely for each property $P$ involving only the symbols of PA and quantifiers over $nn$ add the following axiom:
$P(0) land forall k in nn ( P(k) imp P(k+1) ) imp forall k in nn ( P(k) )$.
Set Theory
Add the type $set$ and the rule that every member of $set$ is also a type.
Add the unary function-symbols $pow,bigcup$, the binary function-symbols $×,FN$, and the constant-symbol $none$. We reuse the binary predicate-symbol $in$, as there will be no ambiguity. Also add the following rules (in every context) for the other notation:
- If $E,F in obj$, then $(E,F) in obj$ and ${E,F} in set$.
- If $S,T in set$, then $S×T in set$ and $FN(S,T) in set$ and $pow(S) in set$.
- If $S,T in set$ and $f in FN(S,T)$ and $x in S$, then $f(x) in T$.
- If $forall x in S ( x in set )$, then $bigcup(S) in set$.
Add the following axioms:
extensionality: $forall S,T in set ( S=T eq forall x in obj ( x in S eq x in T ) ).$
empty-set: $forall x in obj ( neg x in none ).$
power-set: $forall S in set ( pow(S) = { T : T in set land forall x in T ( x in S ) } ).$
pair: $forall x,y in obj ( {x,y} = { z : x=z lor x=y } ).$
ordered-pair: $forall x,y in obj forall z,w in obj ( (x,y)=(z,w) eq x=z land y=w ).$
product-type: $forall S,T in set ( S×T = { t : exists x in S exists y in T ( t=(x,y) ) } ).$
function-type: $forall S,T in set ( FN(S,T) = \ { F : F in S×T land forall x in S exists! y in T ( (x,y) in F ) } ).$
function-application: $forall S,T in set forall f in FN(S,T) forall x in S ( (x,f(x)) in f ).$
union: $forall S in set ( bigcup(S) = { x : exists T in set ( x in T land T in S ) } ).$
choice: $forall S,T in set forall R in S×T ( forall x in S exists y in T ( (x,y) in R ) \ imp exists f in FN(S,T) forall x in S ( (x,f(x)) in R ) ).$
Add the following rules:
type-notation
Take (in the current context) any property $P$ and object expression $E$ and unused variable $x$.
Then ${ x : P(x) }$ is a type and its membership is governed by:
$fitch{}{E in { x : P(x) } eq P(E).}$. ($x$ must not appear in $E$ or $P$)
comprehension
Take any property $P$ and unused variable $x$.
$fitch{S in set.}{{ x : x in S land P(x) } in set.}$. ($x$ must not appear in $S$ or $P$)
collection
Take any $2$-parameter property $P$ and unused variables $x,y$.
$fitch{S in set. \ forall x in S exists y in obj ( P(x,y) ).}{{ y : exists x in S ( P(x,y) ) } in set.}$ ($x,y$ must not appear in $S$ or $P$)
induction
Take any property $P$ with $1$ parameter from $nn$.
$fitch{P(0). \ forall k in nn ( P(k) imp P(k+1) ).}{forall k in nn ( P(k) ).}$ ($k$ must not appear in $P$)
The induction rule subsumes the induction axioms for PA, and essentially the only difference is that the property $P$ can involve set operations and quantification over sets.
function-notation
This rule is theoretically unnecessary but pragmatically very convenient (also known as lambda expressions in computer science).
Take any set $S$ and any object expression $E$ with $1$ parameter from $S$, and unused variable $x$.
Then $( S x mapsto E(x) )$ is an object and its behaviour is governed by:
$fitch{forall x in S ( E(x) in T ). \ f = ( S x mapsto E(x) ).}{f in FN(S,T) land forall x in S ( f(x) = E(x) ).}$
Foundational system
Combining the above Peano Arithmetic plus Set Theory yields a foundational system that is essentially as strong as ZFC but much more user-friendly. It is also agnostic to the existence of objects that are not sets, and does not even assume that the members of $nn$ are sets. It also treats cartesian products and ordered pairs as inbuilt abstract notions. This is how we use them in actual mathematics. (More precisely, the above system directly interprets ZFC minus regularity.)
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
edited Jan 2 at 8:05
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
answered Mar 5 '16 at 14:13
user21820user21820
38.8k543153
38.8k543153
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
add a comment |
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
$begingroup$
Hey man, thanks you very much for all your help :)
$endgroup$
– Jim Jam
Mar 9 '16 at 22:39
1
1
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python.
$endgroup$
– user21820
Mar 10 '16 at 0:57
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
$begingroup$
I decided to update my post with all the rules, and I changed to Python style. The underlying idea is certainly correct, as I've used it for years. But it is a long post and there may be bugs, so if anyone has any question feel free to ask me at chat.stackexchange.com/rooms/44058/logic.
$endgroup$
– user21820
Dec 31 '16 at 17:04
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f1681857%2fpredicate-logic-how-do-you-self-check-the-logical-structure-of-your-own-argumen%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
$begingroup$
There are well-known rules of inference.
$endgroup$
– Hagen von Eitzen
Mar 3 '16 at 19:03
$begingroup$
There are several proof verification software packages that are available free online.
$endgroup$
– Dan Christensen
Mar 4 '16 at 4:53
$begingroup$
Starting from a set of axioms, you can carry out your proof in some Hilbert style deduction system. In fact, "natural" proofs (those that we use on a daily basis) can be thought of as instructions to build a formal deduction in the Hilbert calculus...
$endgroup$
– Stefan Mesken
Mar 5 '16 at 14:26