@Mathmore That's excellent! In my opinion all students need to learn basic logic as it will make logical reasoning (and everything in mathematics) crystal clear, and all fallacies will go away. =)
@Mathmore Here's fine for logic-related stuff. =)
@Mathmore By the way when I teach logic I always include 2 separate stages of explanation of the implication. Since you mention teaching it, you might be interested to know how I do it.
That and the explanation of the chosen semantics. Because most laymen have a different notion of "implies" than the mathematical one, so we need to justify why we are defining the mathematical one in a certain way.
And I never use the English word "implies" in the definition of "⇒".
Now this notion of reasoning within contexts leads directly to Fitch-style natural deduction. There are many variants, and I describe one variant in Math SE (see the links on my profile under natural deduction):
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-preser...
There are many styles of natural deduction, and the one most suited for practical use is Fitch-style, which uses indentation just like programming languages to denote scoping. Basically, you ensure that every sentence you write is true in its context, where the context is captured by headers exac...
It is exactly like in programming, where you have contexts created by if-structures and for/while-loops.
Within each context you can execute statements.
In logic, we don't execute statements, but rather we assert them.
Again recall the goal of logic is to only assert statements that are true within their context. That corresponds exactly to being able to execute the corresponding program with no assertion error.
What happens if P is true? Q had better be true, otherwise it would be wrong. But what happens if P is false? The if-body is not executed so it does not matter what Q is!
This is more or less the second concrete explanation for our choice of semantics for "If P then Q.".
hmmm. since I was teaching for the first time, I gave an explanation which I want to share with you
I taught like this :
If a conditional statement is 'possible' then we give the truth value True to it. Otherwise we say that the statement is false. Lets assume we have a true statement. If we perform logical steps on this statement then the statement to which we arrive has to be true. In other words, it's the only possible way that we start from a true statement and end up on a true statement after doing logical deduction. Since it's 'possible' we assign it's true. let me finish my argument
If we assume a false statement and perform logical deductions on it, then it's possible that we may end up on a true statement or we may end up on a false statement.
I gave examples like if $0=1$ then adding $1$ both sides (which is a logical step), we get $1=2$. So it's possible to start from false statement and end up on a false statement.
Next if $0=1$ then by 'logical step' we have $1=0$ and by adding these two (a 'logical' step) we get $1=1$ which is a true statement. So it's also possible that we start from a false statement and after applying logical deductions we arrive at a true statement.
As discussed, since these things are 'possible' we assign them truth value 'true'.
I stop here. Hope you didn't sleep. Next time I'll definitely include your explanation!
I will advise you to avoid this explanation the next time, because it uses "possible" in a misleading (and technically incorrect) manner. There is a correct way to explain this feature of implication, which I can tell you.
@Mathmore I understood that idea. But you can't use that to justify your first paragraph because your reasoning would then be circular or wrong. If you can prove "p implies q" then indeed you can deduce q logically from p, but not necessarily the other way around!
This may sound crazy, but in any reasonable foundation for mathematics there are sentences P,Q such that: (1) If you can deduce P then you can deduce Q. (2) You cannot deduce ( P implies Q ).
If you take this as true for now, it shows that it is extremely dangerous to associate implication with deduction.
Do you want me to give the details for this 'crazy' claim? Or do you want me to just explain the correct way?
@Mathmore: I've to go off for some time. Let me know what you'd like me to explain further and I'll respond when I'm back.
No no. I didn't mean that if p implies q then q implies p.
I meant if we start from a true statement. apply logical deductions then we get a true statement. I then told them that it is 'never possible' that you apply logical steps on a true statement and end up on a false statement.
I sure want to know your side of the details of this claim. But I didn't mean that this claim is false when teaching the stuff.
I want to know the difference between deduction and implication.
Ignore my first reply "No no..... implies p". I half read your reply and then typed that.
@Mathmore: The details involves the incompleteness theorems. Let FM denote our foundational system for mathematics. Then if FM is sound for arithmetical statements (which we need to believe otherwise we should not be using it) then FM cannot prove some true arithmetical statement Con(FM), where "arithmetical truth" is defined in FM itself. Thus if you can deduce Con(FM) then (vacuously) you can deduce "0=1". But you cannot deduce ( Con(FM) implies 0=1 ).
So this is an explicit example of P,Q such that (1) holds but (2) does not. Therefore, one cannot define the classical implication ( P⇒Q ) to be true exactly when Q can be deduced from P. As in the above example, it may very well be the case that Q can be deduced from P but ( P⇒Q ) is false!
Um, that's the non-trivial part (it was effectively Godel's main contribution). Intuitively we want it to state "FM cannot prove 0=1.". It is relatively easy if we don't want an arithmetical sentence.
I can show you the general idea that produces a sentence about strings instead of natural numbers.
You have come across the halting problem, so there is an interesting easy non-constructive proof of the incompleteness theorems, which I can tell you later. This proof wouldn't serve the purpose of showing you what Con(FM) is like, because it's totally non-constructive. So let's leave that aside first.
Okay. Yeah I have done halting problem in 'theorem-proof' setting. Theorem : There is no algorithm that can tell us whether any given algorithm will loop forever or halt.
To say "FM cannot prove 0=1" we say "There is no string that encodes a proof of 0=1.". Note that a proof in any reasonable formal system can be encoded as a finite string, just like every program is a string.
So Con(FM) can be represented by "¬∃s∈Strings ( ... )" if FM supports string manipulation.
It turns out that if FM can prove Con(FM) then FM can prove "0=1".
Can I support your claim with the following ? Let p : sinx is continuous and q : sinx is differentiable. Now if we can deduce that sinx is continuous then we can deduce that sinx is differentiable. But it's not possible to deduce that "sinx is continuous implies sinx is differentiable."
@Mathmore For any reasonable formal system, it must be, because the only kind of formal systems we can actually use are those that can be described syntactically.
@LeakyNun You are missing the possibility that provability is not the same as truth.
@Mathmore You don't need to know models here. We simply need to work in a foundational system FM that can reason about natural numbers (or finite strings).
The reason I switched to strings is that it's difficult to prove the core Godel lemma needed to get an arithmetical sentence (namely a sentence that only involves natural numbers).
Um, that's the non-trivial part (it was effectively Godel's main contribution). Intuitively we want it to state "FM cannot prove 0=1.". It is relatively easy if we don't want an arithmetical sentence.
I think you meant "FM cannot prove that FM cannot prove that 0=1"?
This may sound crazy, but in any reasonable foundation for mathematics there are sentences P,Q such that: (1) If you can deduce P then you can deduce Q. (2) You cannot deduce ( P implies Q ).
@Mathmore: The details involves the incompleteness theorems. Let FM denote our foundational system for mathematics. Then if FM is sound for arithmetical statements (which we need to believe otherwise we should not be using it) then FM cannot prove some true arithmetical statement Con(FM), where "arithmetical truth" is defined in FM itself. Thus if you can deduce Con(FM) then (vacuously) you can deduce "0=1". But you cannot deduce ( Con(FM) implies 0=1 ).
Um, that's the non-trivial part (it was effectively Godel's main contribution). Intuitively we want it to state "FM cannot prove 0=1.". It is relatively easy if we don't want an arithmetical sentence.
NL (Natural language): This is why I said the answer is yes and no...
Let Con(FM) be the sentence "There is no string encoding a valid proof of 0=1 over FM.".
NL: Of course, "encoding" here is dependent on FM. The easiest way is the generalized way I always do it; a formal system S is simply a program that halts on all input strings and accepts or rejects, and whenever it accepts a pair (p,x) we interpret it to mean that p is a valid proof of sentence x over S.
NL: So that is how we handle formal systems in general. I can hence be now more precise in the definition of Con(FM) in MS.
NL: Remember we will treat FM as a program now.
MS: Let Con(FM) be the sentence ( There is no string p such that FM accepts (p,"0=1"). ).
I edited to avoid ambiguous quotations.
NL: @LeakyNun: Is this definition of Con(FM) clear enough?
I've always interpreted this notion in the following way.
$
\def\eq{\leftrightarrow}
\def\t{\text}
\def\pa{\t{PA}}
\def\th{\t{Th}}
\def\prf{\t{Proof}}
\def\prov{\t{Prov}}
\def\box{\square}
\def\nn{\mathbb{N}}
\def\str#1{{``\text{#1}\!"}}
$
Formal system interpretation
Take any formal systems...
It is symbol-heavy so I will rephrase it in informal terms for Mathmore.
NL: We shall handle formal systems in full generality by considering that each formal system S is simply a program that halts on all string inputs and accepts or rejects, and consider that when a pair (p,x) is accepted it means that p is a valid proof of sentence x over S.
NL: I need to say this in NL because MS cannot possibly talk about our human consideration/interpretation.
MS: Let Con(FM) be the sentence ( There is no string p such that FM accepts (p,"0=1"). ).
NL: Note that pairs can be suitably encoded and decoded by programs. @Mathmore I'm sure you know how to do so, which may involve escaping. Details do not matter here.
NL: We can use NL to study FM, but it's dangerous because NL is ambiguous and people will continually argue about what they mean/say in NL. So to fix that problem we define a syntactic formal system MS that seems to capture how we want to reason about formal systems in general, such as FM.
NL: Most textbooks will not clearly distinguish NL and MS, which is bad in my opinion.
@user21820 asking your opinion before posting it: is this a good question: "in a choiceless universe, if b=inf(A), must there be a sequence in A converging to b"
There is actually a whole spectrum of "formality" in mathematics. In informal terms, "formal" it refers to what is considered as rigorous, but that is of course subjective.
Absolutely formal: Written in a language that can be verified by a program that implements some formal system. Check out M...
A proof in MS would be an absolutely formal proof, while most proofs published by mathematicians would be reasonably formal.
There are many styles of natural deduction, and the one most suited for practical use is Fitch-style, which uses indentation just like programming languages to denote scoping. Basically, you ensure that every sentence you write is true in its context, where the context is captured by headers exac...
You should get the idea; it's actually clear that one can build a program to verify all such proofs.
NL: No I should be precise, otherwise you will later ask why I can say ⬜P is a sentence over FM.
NL: Well by our identification of formal systems and their proof verifier programs, we simply need to say "FM accepts (X,P) for some string X". But how to say "accept"...
@Mathmore NL: we have a bunch of rules that tell you what you can do (such as modus ponens). Then, "FM proves p" is saying that under the rules of FM, there is a sequence of steps such that each consecutive step follows the rules of FM and that the last step is "p".
NL: We shall handle formal systems in full generality by considering that each formal system S is simply a program that halts on all string inputs and accepts or rejects, and consider that when a pair (p,x) is accepted it means that p is a valid proof of sentence x over S.
@Mathmore The thing is that we are defining what it means for a general formal system to prove something. In conventional formal systems you may have syntactic rules of the form "If you can deduce this then you can deduce that." In a general formal system S we define that p is a proof for a sentence x iff S accepts (p,x).
NL: A program execution can be completely encoded as a single finite string (using some suitable encoding+escaping...). So to say that a program accepts some input is the same as saying that there is a finite string that encodes a valid execution of that program on that input that ends in acceptance.
MS: Let ⬜P denote the sentence "There is a string E and proof C such that E is a valid encoding of the execution of FM on (C,P) that ends with acceptance.", for any sentence P over FM.
MS: Then ⬜P is actually a sentence over FM. (NL: Because we chose that FM can form sentences about strings.)
MS: Given any sentence P over FM we have the following: (D1) If FM proves P then FM proves ⬜P. (D2) FM proves ( ⬜P∧⬜(P⇒Q)⇒⬜Q ). (Note that the precedence order from highest to lowest is ⬜,∧,⇒.) (D3) FM proves ( ⬜P⇒⬜⬜P ).
@Mathmore I'm being a little imprecise up there. ⬜P is a mostly English sentence... However, you can see that you can translate it into a sentence over FM. Let me be a bit more precise...
Definitions
$x\text{ is even} := \exists y[y+y=x]$ (Denote as $E(x)$)
$x\text{ is odd} := \exists y[S(y+y)=x]$ (Denote as $O(x)$)
Axioms
$\forall x[S(x) \ne 0]$
$\forall x \forall y[S(x)=S(y) \implies x=y]$
$\forall x[x+0=x]$
$\forall x \forall y[x+S(y)=S(x+y)]$
$[\varphi(0) \land [\forall ...
