info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Reductio Ad Absurdum (RAA) missing in DC Proof
191 views
Skip to first unread message
Mostowski Collapse
Mar 19, 2023, 2:41:02 PM3/19/23
to
Now I wanted to redo some proofs here:
http://pravda.irisa.fr/naturaldeduction.html
But already this inference rule (RAA) is missing in DC Proof:
G, ~A |- f
---------------
G |- A
The problem is seen here, here is a proof with RAA:
|___~~p
| |___~p
| | ~~p (R)
| | ~p (R)
| | f (->E)
| p (D)
~~p -> p (->I)
In DC Proof I need a double negation elimination (DNE)
step, which is nonsense, since I want to verify DNE from RAA:
1 ~~P
Premise
2 ~P
Premise
3 ~~P & ~P
Join, 1, 2
4 ~~P
Conclusion, 2
5 P
Rem DNeg, 4
6 ~~P => P
Conclusion, 1
So its not possible to prove ~~P => P in DC Proof,
from RAA without using DNE?
http://pravda.irisa.fr/naturaldeduction.html
But already this inference rule (RAA) is missing in DC Proof:
G, ~A |- f
---------------
G |- A
The problem is seen here, here is a proof with RAA:
|___~~p
| |___~p
| | ~~p (R)
| | ~p (R)
| | f (->E)
| p (D)
~~p -> p (->I)
In DC Proof I need a double negation elimination (DNE)
step, which is nonsense, since I want to verify DNE from RAA:
1 ~~P
Premise
2 ~P
Premise
3 ~~P & ~P
Join, 1, 2
4 ~~P
Conclusion, 2
5 P
Rem DNeg, 4
6 ~~P => P
Conclusion, 1
So its not possible to prove ~~P => P in DC Proof,
from RAA without using DNE?
Dan Christensen
Mar 19, 2023, 3:31:16 PM3/19/23
to
On Sunday, March 19, 2023 at 2:41:02 PM UTC-4, Mostowski Collapse wrote:
> Now I wanted to redo some proofs here:
>
> http://pravda.irisa.fr/naturaldeduction.html
>
> But already this inference rule (RAA) is missing in DC Proof:
>
> G, ~A |- f
> ---------------
> G |- A
>
Proof by Contradiction (RAA) is built into the Conclusion Rule.
> Now I wanted to redo some proofs here:
>
> http://pravda.irisa.fr/naturaldeduction.html
>
> But already this inference rule (RAA) is missing in DC Proof:
>
> G, ~A |- f
> ---------------
> G |- A
>
> The problem is seen here, here is a proof with RAA:
>
> |___~~p
> | |___~p
> | | ~~p (R)
> | | ~p (R)
> | | f (->E)
> | p (D)
> ~~p -> p (->I)
>
> In DC Proof I need a double negation elimination (DNE)
> step, which is nonsense, since I want to verify DNE from RAA:
>
> 1 ~~P
> Premise
>
> 2 ~P
> Premise
>
> 3 ~~P & ~P
> Join, 1, 2
>
> 4 ~~P
> Conclusion, 2
>
> 5 P
> Rem DNeg, 4
>
> 6 ~~P => P
> Conclusion, 1
>
> So its not possible to prove ~~P => P in DC Proof,
> from RAA without using DNE?
1. ~~P
Premise
2. P
Rem DNeg, 1
3. ~~P => P
Conclusion, 1
Nothing to do with proof by contradiction.
Here is the simplest proof by contradiction:
1. P & ~P
Premise
2. ~[P & ~P]
Conclusion, 1
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
Mar 19, 2023, 4:26:02 PM3/19/23
to
Where do you show from Reductio Ad Absurdum (RAA)
without using double negation elimination (DNE)?
This here is not from RAA without DNE:
> 1. ~~P
> Premise
>
> 2. P
> Rem DNeg, 1
>
> 3. ~~P => P
> Conclusion, 1
It has exactly DNE in step 2.
without using double negation elimination (DNE)?
This here is not from RAA without DNE:
> 1. ~~P
> Premise
>
> 2. P
> Rem DNeg, 1
>
> 3. ~~P => P
> Conclusion, 1
Mostowski Collapse
Mar 19, 2023, 4:34:27 PM3/19/23
to
Thats the error in your tool, in that it doesn't provide
RAA, it only provides "not introduction":
> > 4 ~~P
> > Conclusion, 2
> You are back to where you started, Mr. Collapse!
If it would have proper RAA, we would get:
> > 4 P
> > Conclusion, 2
Proper RAA is described by Euclid:
"Every reduction to impossibility takes the contradictory
of what it intends to prove and from this as a hypothesis
proceeds until it encounters something admitted to be
absurd and, by thus destroying its hypothesis, confirm
the proposition it set out to establish."
Which is this inference rule, which is
exactly RAA as per Euclid:
> G, ~A |- f
> ---------------
> G |- A
But your tool provides this inference rule,
which is not exactly RAA as per Euclid:
> G, A |- f
> ---------------
> G |- ~A
RAA, it only provides "not introduction":
> > 4 ~~P
> > Conclusion, 2
> You are back to where you started, Mr. Collapse!
> > 4 P
> > Conclusion, 2
Proper RAA is described by Euclid:
"Every reduction to impossibility takes the contradictory
of what it intends to prove and from this as a hypothesis
proceeds until it encounters something admitted to be
absurd and, by thus destroying its hypothesis, confirm
the proposition it set out to establish."
Which is this inference rule, which is
exactly RAA as per Euclid:
> G, ~A |- f
> ---------------
> G |- A
which is not exactly RAA as per Euclid:
> G, A |- f
> ---------------
> G |- ~A
Dan Christensen
Mar 19, 2023, 5:52:52 PM3/19/23
to
> Where do you show from Reductio Ad Absurdum (RAA)
> without using double negation elimination (DNE)?
The Conclusion Rule looks at the last active premise (line 1) and preceding line (also line 1 in this case). If the preceding line is a contradiction of the form "A & ~A" or "A <=> ~A", then it generates a conclusion that is the negation of the last active premise, and discharges that premise. In this case, the preceding line (line 1) is a contradiction.
> without using double negation elimination (DNE)?
> This here is not from RAA without DNE:
> > 1. ~~P
> > Premise
> >
> > 2. P
> > Rem DNeg, 1
> >
> > 3. ~~P => P
> > Conclusion, 1
> It has exactly DNE in step 2.
Mostowski Collapse
Mar 19, 2023, 6:15:06 PM3/19/23
to
I don't know whether its a direct proof. What do you
mean by direct proof? Its surely not a proof that uses RAA.
Since you somehow swept RAA under the rug:
You claimed verbatim "Proof by Contradiction (RAA)
is built into the Conclusion Rule." How? Your Conclusion
Rule is only this here:
> G, A |- B & ~B
> ---------------
> G |- ~A
And not this here:
> G, ~A |- B & ~B
> ---------------
> G |- A
You are subject to a novice confusion:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
mean by direct proof? Its surely not a proof that uses RAA.
Since you somehow swept RAA under the rug:
You claimed verbatim "Proof by Contradiction (RAA)
is built into the Conclusion Rule." How? Your Conclusion
Rule is only this here:
> G, A |- B & ~B
> ---------------
> G |- ~A
And not this here:
> G, ~A |- B & ~B
> ---------------
> G |- A
You are subject to a novice confusion:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
Dan Christensen
Mar 19, 2023, 6:42:13 PM3/19/23
to
On Sunday, March 19, 2023 at 6:15:06 PM UTC-4, Mostowski Collapse wrote:
> Dan Christensen schrieb am Sonntag, 19. März 2023 um 22:52:52 UTC+1:
> > > This here is not from RAA without DNE:
> > > > 1. ~~P
> > > > Premise
> > > >
> > > > 2. P
> > > > Rem DNeg, 1
> > > >
> > > > 3. ~~P => P
> > > > Conclusion, 1
> > > It has exactly DNE in step 2.
> > Correct. There is no need for proof by contradiction (RAA) here. It is a direct proof.
> Dan Christensen schrieb am Sonntag, 19. März 2023 um 22:52:52 UTC+1:
> > > This here is not from RAA without DNE:
> > > > 1. ~~P
> > > > Premise
> > > >
> > > > 2. P
> > > > Rem DNeg, 1
> > > >
> > > > 3. ~~P => P
> > > > Conclusion, 1
> > > It has exactly DNE in step 2.
> > Correct. There is no need for proof by contradiction (RAA) here. It is a direct proof.
> I don't know whether its a direct proof. What do you
> mean by direct proof?
A direct (or conditional) proof is one that is neither a proof by contradiction, a proof by contrapositive nor a proof by cases. It is a straightforward proof of a conditional statement.
> mean by direct proof?
> Its surely not a proof that uses RAA.
> Since you somehow swept RAA under the rug:
>
> You claimed verbatim "Proof by Contradiction (RAA)
> is built into the Conclusion Rule." How? Your Conclusion
> Rule is only this here:
>
> > G, A |- B & ~B
> > ---------------
> > G |- ~A
>
> And not this here:
>
> > G, ~A |- B & ~B
> > ---------------
> > G |- A
>
Mostowski Collapse
Mar 19, 2023, 6:53:10 PM3/19/23
to
How would you prove this one:
((p -> q) -> p) -> p
((p -> q) -> p) -> p
Mostowski Collapse
Mar 19, 2023, 9:33:53 PM3/19/23
to
Can you prove it in less than 12 steps?
Dan Christensen
Mar 19, 2023, 10:12:47 PM3/19/23
to
On Sunday, March 19, 2023 at 6:53:10 PM UTC-4, Mostowski Collapse wrote:
> How would you prove this one:
>
> ((p -> q) -> p) -> p
See my reply just now to your identical posting at sci.math
> How would you prove this one:
>
> ((p -> q) -> p) -> p
Dan
Mostowski Collapse
Mar 20, 2023, 3:42:40 PM3/20/23
to
Well the "Reductio" is only a short hand to your
combination of "Conclusion" and "Rem DNeg".
So instead Reductio:
> > 10 p
> > Reductio 2,9
In your System it would read:
> > 10 ~~p
> > Conclusion, 2
> >
> > 11 p
> > Rem DNeg, 10
Obviously my System saves one Rem DNeg application.
Therefore since the proof of (p -> q) -> p) -> p has two
Reductio, it is two steps shorter.
One can also show that in the presence "Reductio",
no Rem DNeg is needed at all! Since the Calculus
having Reduction and no Rem DNeg is complete:
See also, it has a chapter Completness:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
combination of "Conclusion" and "Rem DNeg".
So instead Reductio:
> > 10 p
> > Reductio 2,9
In your System it would read:
> > 10 ~~p
> > Conclusion, 2
> >
> > 11 p
> > Rem DNeg, 10
Obviously my System saves one Rem DNeg application.
Therefore since the proof of (p -> q) -> p) -> p has two
Reductio, it is two steps shorter.
One can also show that in the presence "Reductio",
no Rem DNeg is needed at all! Since the Calculus
having Reduction and no Rem DNeg is complete:
See also, it has a chapter Completness:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
Mostowski Collapse
Mar 20, 2023, 3:53:09 PM3/20/23
to
That DNE is redundant, when there is RAA, was
what I intially posted here:
Mostowski Collapse schrieb am Sonntag, 19. März 2023 um 19:42:59 UTC+1:
> |___~~p
> | |___~p
> | | ~~p (R)
> | | ~p (R)
> | | f (->E)
> | p (D)
> ~~p -> p (->I)
https://groups.google.com/g/sci.math/c/OFS80kbpVcU/m/U1kpO5SXAgAJ
Or more readable in DC Proof style:
1 ~~p
Premise
2 ~p
Premise
3 ~~p & ~p
Join 1,2
4 p
Reductio 2,3
5 ~~p -> p
Conclusion 1,4
In your system you need 6 steps, and DNE. But we want
to show DNE redundant. This is I guess not possible
in your system. To show DNE from some first principles?
what I intially posted here:
Mostowski Collapse schrieb am Sonntag, 19. März 2023 um 19:42:59 UTC+1:
> |___~~p
> | |___~p
> | | ~~p (R)
> | | ~p (R)
> | | f (->E)
> | p (D)
> ~~p -> p (->I)
Or more readable in DC Proof style:
1 ~~p
Premise
2 ~p
Premise
3 ~~p & ~p
Join 1,2
4 p
Reductio 2,3
5 ~~p -> p
Conclusion 1,4
In your system you need 6 steps, and DNE. But we want
to show DNE redundant. This is I guess not possible
in your system. To show DNE from some first principles?
Dan Christensen
Mar 20, 2023, 4:44:29 PM3/20/23
to
See my reply just now to your identical posting in sci.math
Dan
Dan
Mostowski Collapse
Mar 20, 2023, 5:38:46 PM3/20/23
to
Thats probably the most deranged answer I have ever seen:
> Better would be:
> Better would be:
> 1. ~~P
> Premise
> 2. P
> Rem DNeg, 1
> 3. ~~P => P
> Conclusion, 1
How is this a proof of DNE that doesn't use Rem DNeg?
> Premise
> 2. P
> Rem DNeg, 1
> 3. ~~P => P
> Conclusion, 1
Mostowski Collapse
Mar 20, 2023, 5:41:28 PM3/20/23
to
Well if you have a board in front of the head, you
shouldn't use any proof system at all.
Well it would be a system for less "novice" users. Like
dumbos like yourself wouldn't use such a system. Here
its already online, including collapse/expand of subproofs:
Example 94: Collapsible DC Proof
https://www.dogelog.ch/littab/moblet/docs/05_supplement/03_redux/example94/package.html
You see the first proof doesn't use "Reductio", so
its a proof valid in minimal logic:
8 (p -> q) -> (q -> r) -> p -> r
▶ Conclusion 1,7
And the second proof does use "Reductio", so
its a proof that makes use of classical logic principles:
11 ((p -> q) -> p) -> p
▶ Conclusion 1,10
Hope this Helps! But not you, you are a dumbo, cant
tell apart "Conclusion" and "Reductio", so its nothing
for you Dan Christensen. Its more for the educated
populace of this planet, and not the uneducated that
can even not tell apart classical and non-classical logic.
Non-constructive logic and constructive logic.
LoL
Dan Christensen schrieb am Montag, 20. März 2023 um 21:29:45 UTC+1:
> Better that than introduce a additional rule to potentially confuse users.
shouldn't use any proof system at all.
Well it would be a system for less "novice" users. Like
dumbos like yourself wouldn't use such a system. Here
its already online, including collapse/expand of subproofs:
Example 94: Collapsible DC Proof
https://www.dogelog.ch/littab/moblet/docs/05_supplement/03_redux/example94/package.html
You see the first proof doesn't use "Reductio", so
its a proof valid in minimal logic:
8 (p -> q) -> (q -> r) -> p -> r
▶ Conclusion 1,7
And the second proof does use "Reductio", so
its a proof that makes use of classical logic principles:
11 ((p -> q) -> p) -> p
▶ Conclusion 1,10
Hope this Helps! But not you, you are a dumbo, cant
tell apart "Conclusion" and "Reductio", so its nothing
for you Dan Christensen. Its more for the educated
populace of this planet, and not the uneducated that
can even not tell apart classical and non-classical logic.
Non-constructive logic and constructive logic.
LoL
Dan Christensen schrieb am Montag, 20. März 2023 um 21:29:45 UTC+1:
> Better that than introduce a additional rule to potentially confuse users.
Dan Christensen
Mar 20, 2023, 9:51:39 PM3/20/23
to
On Monday, March 20, 2023 at 5:38:46 PM UTC-4, Mostowski Collapse wrote:
> Thats probably the most deranged answer I have ever seen:
>
> > Better would be:
> > 1. ~~P
> > Premise
> > 2. P
> > Rem DNeg, 1
> > 3. ~~P => P
> > Conclusion, 1
Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> Thats probably the most deranged answer I have ever seen:
>
> > Better would be:
> > 1. ~~P
> > Premise
> > 2. P
> > Rem DNeg, 1
> > 3. ~~P => P
> > Conclusion, 1
Dan
Julio Di Egidio
Mar 21, 2023, 12:58:09 AM3/21/23
to
Julio
Dan Christensen
Mar 21, 2023, 1:18:50 AM3/21/23
to
On Monday, March 20, 2023 at 3:53:09 PM UTC-4, Mostowski Collapse wrote:
[snip]
> But we want
> to show DNE redundant.
Why? Even if, in some sense, it could be shown to be "redundant", users would still legitimately insist on a rule of inference to eliminate double negations as a "shortcut" if not technically an axiom. You are grasping at straws here, Mr. Collapse.
See: https://en.wikipedia.org/wiki/Double_negation#Elimination_and_introduction
[snip]
> But we want
> to show DNE redundant.
See: https://en.wikipedia.org/wiki/Double_negation#Elimination_and_introduction
Dan Christensen
Mar 21, 2023, 1:30:58 AM3/21/23
to
Dan
Mostowski Collapse
Mar 21, 2023, 7:42:22 AM3/21/23
to
How would you proove:
((p -> q) -> p) -> p
Only using implication rules and negation rules?
No disjunction and conjunction rules allowed?
((p -> q) -> p) -> p
No disjunction and conjunction rules allowed?
Mostowski Collapse
Mar 21, 2023, 7:50:47 AM3/21/23
to
Ok, I got this one. Got a new proof finder which
doesn't search for RAA, but for DNE. Again its doing
backward search. This can be also used as a lackmus
paper for a non-classical versus classical proof.
The only non-implication or non-negation used,
is the DC Proof Join to derive a contradiction:
1 (p -> q) -> p
Premise
2 ~p
Premise
3 p
Premise
4 ~q
Premise
5 ~p & p
Join 2,3
6 ~~q
Conclusion 4,5
7 q
Rem DNeg 6
8 p -> q
Conclusion 3,7
9 p
Detach 1,8
10 ~p & p
Join 2,9
11 ~~p
Conclusion 2,10
12 p
Rem DNeg 11
13 ((p -> q) -> p) -> p
Conclusion 1,12
doesn't search for RAA, but for DNE. Again its doing
backward search. This can be also used as a lackmus
paper for a non-classical versus classical proof.
The only non-implication or non-negation used,
is the DC Proof Join to derive a contradiction:
1 (p -> q) -> p
Premise
2 ~p
Premise
3 p
Premise
4 ~q
Premise
5 ~p & p
Join 2,3
6 ~~q
Conclusion 4,5
7 q
Rem DNeg 6
8 p -> q
Conclusion 3,7
9 p
Detach 1,8
10 ~p & p
Join 2,9
11 ~~p
Conclusion 2,10
12 p
Rem DNeg 11
13 ((p -> q) -> p) -> p
Conclusion 1,12
Julio Di Egidio
Mar 21, 2023, 8:02:37 AM3/21/23
to
Julio
Julio Di Egidio
Mar 21, 2023, 8:14:54 AM3/21/23
to
On Tuesday, 21 March 2023 at 12:50:47 UTC+1, Mostowski Collapse wrote:
> Ok, I got this one. Got a new proof finder which
> doesn't search for RAA, but for DNE. Again its doing
> backward search. This can be also used as a lackmus
>
> paper for a non-classical versus classical proof.
> The only non-implication or non-negation used,
> is the DC Proof Join to derive a contradiction:
>
> 1 (p -> q) -> p
> Premise
That statement is equivalent to LEM as well as
> Ok, I got this one. Got a new proof finder which
> doesn't search for RAA, but for DNE. Again its doing
> backward search. This can be also used as a lackmus
>
> paper for a non-classical versus classical proof.
> The only non-implication or non-negation used,
> is the DC Proof Join to derive a contradiction:
>
> 1 (p -> q) -> p
> Premise
equivalent to DNE and to some others. I had
given you a link...
That said, I am curious: how do you go from there
to 2, 3 and 4 below? (2 and 3 look like an application
of LEM, but then I do not see how you also get 4.)
> 2 ~p
> Premise
>
> 3 p
> Premise
>
> 4 ~q
> Premise
Julio Di Egidio
Mar 21, 2023, 8:18:08 AM3/21/23
to
On Tuesday, 21 March 2023 at 13:14:54 UTC+1, Julio Di Egidio wrote:
> On Tuesday, 21 March 2023 at 12:50:47 UTC+1, Mostowski Collapse wrote:
> > Ok, I got this one. Got a new proof finder which
> > doesn't search for RAA, but for DNE. Again its doing
> > backward search. This can be also used as a lackmus
> >
> > paper for a non-classical versus classical proof.
> > The only non-implication or non-negation used,
> > is the DC Proof Join to derive a contradiction:
> >
> > 1 (p -> q) -> p
> > Premise
> That statement is equivalent to LEM as well as
> equivalent to DNE and to some others. I had
> given you a link...
No, sorry, the one equivalent to LEM is
> On Tuesday, 21 March 2023 at 12:50:47 UTC+1, Mostowski Collapse wrote:
> > Ok, I got this one. Got a new proof finder which
> > doesn't search for RAA, but for DNE. Again its doing
> > backward search. This can be also used as a lackmus
> >
> > paper for a non-classical versus classical proof.
> > The only non-implication or non-negation used,
> > is the DC Proof Join to derive a contradiction:
> >
> > 1 (p -> q) -> p
> > Premise
> That statement is equivalent to LEM as well as
> equivalent to DNE and to some others. I had
> given you a link...
((P -> Q) -> P) -> P, so called Pierce's law.
Mostowski Collapse
Mar 21, 2023, 8:21:10 AM3/21/23
to
Premises are just input into the proof system. You are free in Natural
Deduction to input any premise you want. This is also how
DC Proof works. They remain until they get discharged by a conclusion
statement. So in line 4 a premise is introduced:
4 ~q
Premise
And this premise gets discharged in line:
6 ~~q
Conclusion 4,5
Some for the other premises. They all get eventually discharged,
until there are no more premises, only what one wanted
to prove. See also here maybe:
What does discharging an assumption mean in Natural Deduction?
https://math.stackexchange.com/questions/3527285/what-does-discharging-an-assumption-mean-in-natural-deduction
Deduction to input any premise you want. This is also how
DC Proof works. They remain until they get discharged by a conclusion
statement. So in line 4 a premise is introduced:
4 ~q
Premise
And this premise gets discharged in line:
6 ~~q
Conclusion 4,5
Some for the other premises. They all get eventually discharged,
until there are no more premises, only what one wanted
to prove. See also here maybe:
What does discharging an assumption mean in Natural Deduction?
https://math.stackexchange.com/questions/3527285/what-does-discharging-an-assumption-mean-in-natural-deduction
Julio Di Egidio
Mar 21, 2023, 8:27:43 AM3/21/23
to
On Tuesday, 21 March 2023 at 13:21:10 UTC+1, Mostowski Collapse wrote:
> Premises are just input into the proof system. You are free in Natural
> Deduction to input any premise you want. This is also how
> DC Proof works. They remain until they get discharged by a conclusion
>
> statement. So in line 4 a premise is introduced:
>
> 4 ~q
> Premise
>
> And this premise gets discharged in line:
>
> 6 ~~q
> Conclusion 4,5
>
> Some for the other premises. They all get eventually discharged,
> until there are no more premises, only what one wanted
> to prove.
So, that's all RAA under the name of "premises" if I get it right.
> Premises are just input into the proof system. You are free in Natural
> Deduction to input any premise you want. This is also how
> DC Proof works. They remain until they get discharged by a conclusion
>
> statement. So in line 4 a premise is introduced:
>
> 4 ~q
> Premise
>
> And this premise gets discharged in line:
>
> 6 ~~q
> Conclusion 4,5
>
> Some for the other premises. They all get eventually discharged,
> until there are no more premises, only what one wanted
> to prove.
Tsk tsk... ;)
Julio
Mostowski Collapse
Mar 21, 2023, 8:27:52 AM3/21/23
to
Recently I started interpreting Peirce's law:
((P -> Q) -> P) -> P
The following way. First observe that it seems that
disjunction can be view as follows. Didn't Peirce anyway
juggle with this, and thats how he came up with his Law?
A v B <-> ((A -> B) -> B)
Although Wikipedia cites other passages from Peirce.
Not sure, minimal logic, intuitionistic logic, classical
logic valid. You have to check.
But Peirce's Law then translates to:
(P -> Q) v P
Which has LEM as a special case with Q=f, in
case your logic has a Falsum f, and in case you allow
~P interpreted as P -> f.
((P -> Q) -> P) -> P
disjunction can be view as follows. Didn't Peirce anyway
juggle with this, and thats how he came up with his Law?
A v B <-> ((A -> B) -> B)
Although Wikipedia cites other passages from Peirce.
Not sure, minimal logic, intuitionistic logic, classical
logic valid. You have to check.
But Peirce's Law then translates to:
(P -> Q) v P
Which has LEM as a special case with Q=f, in
case your logic has a Falsum f, and in case you allow
~P interpreted as P -> f.
Mostowski Collapse
Mar 21, 2023, 8:36:24 AM3/21/23
to
Eitherway you cannot prove Peirce Law without
RAA or without DNE. Thats the whole point of
Peirce Law.
But I do not use RAA anymore, I have abandoned RAA.
And Premise is from DC Proof (~Intro). You see
also the Premise Label in DC Proof. Its not something
I have invented. RAA is this inference rule, it removes
a negation. It made use of a Premise Label, but as
I said I do not support RAA anymore. It had a label
in the end "Reductio":
/* before you have negation ~A, after you have
no more negation A */
G, ~A |- f
---------------- (RAA)
G |- A
Now we are back to DC Proofs Conclusion Rule
only, which introduces a negation. It has also a
Premise Label, but a differnet label in the end.
Its the label "Conclusion" adopted from DC Proof:
/* before you have no negation A, after you have
negation introduced ~A */
G, A |- f
---------------- (~ Intro)
G |- ~A
If you want remove negation, you can do that
if they come in a double pack, thats the DNE rule,
which I now support to be more compatible with DC Proof,
it has the label "Rem DNeg" adopted from DC Proof:
G |- ~~A
---------------- (DNE)
G |- A
In case you are still interested in RAA, which I have
abandoned, but still if you would be interested, its
relatively easy to see that RAA = ~Intro + DNE.
RAA or without DNE. Thats the whole point of
Peirce Law.
But I do not use RAA anymore, I have abandoned RAA.
And Premise is from DC Proof (~Intro). You see
also the Premise Label in DC Proof. Its not something
I have invented. RAA is this inference rule, it removes
a negation. It made use of a Premise Label, but as
I said I do not support RAA anymore. It had a label
in the end "Reductio":
/* before you have negation ~A, after you have
no more negation A */
G, ~A |- f
---------------- (RAA)
G |- A
Now we are back to DC Proofs Conclusion Rule
only, which introduces a negation. It has also a
Premise Label, but a differnet label in the end.
Its the label "Conclusion" adopted from DC Proof:
/* before you have no negation A, after you have
negation introduced ~A */
G, A |- f
---------------- (~ Intro)
G |- ~A
If you want remove negation, you can do that
if they come in a double pack, thats the DNE rule,
which I now support to be more compatible with DC Proof,
it has the label "Rem DNeg" adopted from DC Proof:
G |- ~~A
---------------- (DNE)
G |- A
In case you are still interested in RAA, which I have
abandoned, but still if you would be interested, its
relatively easy to see that RAA = ~Intro + DNE.
Dan Christensen
Mar 21, 2023, 9:42:33 AM3/21/23
to
On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
> > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> >
> > > In school one should rather learn that there is nothing innocent about that.
> >
> > That would be a disservice to students.
> That is only a disservice to [snip childish abuse] you.
> > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> >
> > > In school one should rather learn that there is nothing innocent about that.
> >
> > That would be a disservice to students.
>
Come now! You can play these games with consenting adults, but would you really tell a 12-year-old that there is something ambiguous about the sentence, "It is false that it is not raining?"
Julio Di Egidio
Mar 21, 2023, 9:46:22 AM3/21/23
to
On Tuesday, 21 March 2023 at 13:36:24 UTC+1, Mostowski Collapse wrote:
> And Premise is from DC Proof (~Intro). You see
> also the Premise Label in DC Proof. Its not something
> I have invented. RAA is this inference rule, it removes
> a negation. It made use of a Premise Label, but as
> I said I do not support RAA anymore. It had a label
>
> in the end "Reductio":
>
> /* before you have negation ~A, after you have
> no more negation A */
> G, ~A |- f
> ---------------- (RAA)
> G |- A
>
> Now we are back to DC Proofs Conclusion Rule
> only, which introduces a negation. It has also a
> Premise Label, but a differnet label in the end.
>
> Its the label "Conclusion" adopted from DC Proof:
>
> /* before you have no negation A, after you have
> negation introduced ~A */
> G, A |- f
> ---------------- (~ Intro)
> G |- ~A
>
> If you want remove negation, you can do that
> if they come in a double pack, thats the DNE rule,
>
> And Premise is from DC Proof (~Intro). You see
> also the Premise Label in DC Proof. Its not something
> I have invented. RAA is this inference rule, it removes
> a negation. It made use of a Premise Label, but as
> I said I do not support RAA anymore. It had a label
>
> in the end "Reductio":
>
> /* before you have negation ~A, after you have
> no more negation A */
> G, ~A |- f
> ---------------- (RAA)
> G |- A
>
> Now we are back to DC Proofs Conclusion Rule
> only, which introduces a negation. It has also a
> Premise Label, but a differnet label in the end.
>
> Its the label "Conclusion" adopted from DC Proof:
>
> /* before you have no negation A, after you have
> negation introduced ~A */
> G, A |- f
> ---------------- (~ Intro)
> G |- ~A
>
> If you want remove negation, you can do that
> if they come in a double pack, thats the DNE rule,
>
> In case you are still interested in RAA, which I have
> abandoned, but still if you would be interested, its
> relatively easy to see that RAA = ~Intro + DNE.
That is all quite wrong and messed up, to begin with
> abandoned, but still if you would be interested, its
> relatively easy to see that RAA = ~Intro + DNE.
that is not RAA. Indeed you also miss the point of my
remark: that you are (or were) looking for something
(RAA) that is under your nose.
That said, what you are calling ~Intro is what I have called
de-intro and is utterly innocuous, as well as the equivalence
~P to P->False, which is by Curry-Howard. Whence you are
saying RAA <-> DNE (<-> LEM <-> Pierce's <-> few other ways
to say it). But RAA =/= DNE, not per chance RAA is not a
problem in constructive logic, bringing *arbitrary* hypothesis
into existence is.
<https://users.cecs.anu.edu.au/~jks/LogicNotes/RAA.html>
Anyway, enough said.
Julio
Julio Di Egidio
Mar 21, 2023, 10:23:14 AM3/21/23
to
On Tuesday, 21 March 2023 at 14:42:33 UTC+1, Dan Christensen wrote:
> On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
>
> > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > >
> > > > In school one should rather learn that there is nothing innocent about that.
> > >
> > > That would be a disservice to students.
> > That is only a disservice to [snip childish abuse] you.
>
> Come now! You can play these games with consenting adults,
Go fuck yourself.
> On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
>
> > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > >
> > > > In school one should rather learn that there is nothing innocent about that.
> > >
> > > That would be a disservice to students.
> > That is only a disservice to [snip childish abuse] you.
>
> Come now! You can play these games with consenting adults,
> but would you really tell a 12-year-old that there is something
> ambiguous about the sentence, "It is false that it is not raining?"
raining, then it is indeed not raining". But [~~R -> R] means that
"if you do not see that it is not raining, then you can conclude
that it is raining", which is altogether in another league...
Julio
Mostowski Collapse
Mar 21, 2023, 10:24:53 AM3/21/23
to
Its relatively trivial, ~Intro + DNE = RAA:
G, ~A |- f
---------------- (~ Intro)
of (~Intro) and the Lego piece (DNE) together,
and you get the Lego piece (RAA):
G, ~A |- f
---------------- (RAA)
G |- A
Thats not some secret. You find this all over the internet.
110 years of formal Logic, and the many "movements"
needed it understand it, pretty much match the 90 years of Lego:
90 Years of LEGO® Play
https://www.youtube.com/watch?v=CcI2ykaNXd8
G, ~A |- f
---------------- (~ Intro)
G |- ~~A
---------------- (DNE)
G |- A
Its just like playing with Lego. Put the Lego piece
---------------- (DNE)
G |- A
of (~Intro) and the Lego piece (DNE) together,
and you get the Lego piece (RAA):
G, ~A |- f
---------------- (RAA)
G |- A
110 years of formal Logic, and the many "movements"
needed it understand it, pretty much match the 90 years of Lego:
90 Years of LEGO® Play
https://www.youtube.com/watch?v=CcI2ykaNXd8
Mostowski Collapse
Mar 21, 2023, 10:39:29 AM3/21/23
to
For development of search algorithm the G |- A notation
is more handy. But you can write it also like this,
indicating the discharge via [A]:
[~A]
.
.
.
f
-------- (RAA)
A
And the combination of (~Intro) applied to (~A)
and then (DNE):
[~A]
.
.
.
f
-------- (~Intro)
~~A
------- (DNE)
A
For more details see Page 31 ff, this author tends to
use the alternative notation of discharge via [A]:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
is more handy. But you can write it also like this,
indicating the discharge via [A]:
[~A]
.
.
.
f
-------- (RAA)
A
And the combination of (~Intro) applied to (~A)
and then (DNE):
[~A]
.
.
.
f
-------- (~Intro)
~~A
------- (DNE)
A
For more details see Page 31 ff, this author tends to
use the alternative notation of discharge via [A]:
‘a confusion of novice’ to call both schemas Reductio ad Absurdum
van Dalen, D. (2008), Logic and Structure, Springer-Verlag.
https://www.cin.ufpe.br/~mlogica/livros/Logic%20and%20Structure%20-%20Van%20Dalen.pdf
Dan Christensen
Mar 21, 2023, 10:45:33 AM3/21/23
to
On Tuesday, March 21, 2023 at 10:23:14 AM UTC-4, Julio Di Egidio wrote:
> On Tuesday, 21 March 2023 at 14:42:33 UTC+1, Dan Christensen wrote:
> > On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
> >
> > > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > > >
> > > > > In school one should rather learn that there is nothing innocent about that.
> > > >
> > > > That would be a disservice to students.
> > > That is only a disservice to [snip childish abuse] you.
> >
> > Come now! You can play these games with consenting adults,
[snip childish abuse]
> On Tuesday, 21 March 2023 at 14:42:33 UTC+1, Dan Christensen wrote:
> > On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
> >
> > > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > > >
> > > > > In school one should rather learn that there is nothing innocent about that.
> > > >
> > > > That would be a disservice to students.
> > > That is only a disservice to [snip childish abuse] you.
> >
> > Come now! You can play these games with consenting adults,
> > but would you really tell a 12-year-old that there is something
> > ambiguous about the sentence, "It is false that it is not raining?"
> Is simply trivial that [~R -> ~R], i.e. that "if you see that it is not
> raining, then it is indeed not raining". But [~~R -> R] means that
> "if you do not see that it is not raining, then you can conclude
> that it is raining", which is altogether in another league...
>
Mostowski Collapse
Mar 21, 2023, 10:49:50 AM3/21/23
to
By the standard of van Dalen, Figure 3.5.1.2 of John
John Slaney is not RAA. Since it introduces a negation.
It goes from B to ~B. But for RAA you need to go from
~B to B, read Euclid below carefully!
X, B ⊢ A
Y, B ⊢ ¬A
---------------------- (Wrong Label RAA, should say ~Intro)
X, Y ⊢ ¬B
Figure 3.5.1.2
So maybe van Dalen should have written "Novice"
and "Grown Ups" make this error. That they cannot
distingish RAA from ~Intro.
Well, we don't live in a perfect world. This is a fast
paced world, where everybody can put any nonsense
on the internet. Even if he didn't understand Euclid:
"Every reduction to impossibility takes the contradictory
of what it intends to prove and from this as a hypothesis
proceeds until it encounters something admitted to be
absurd and, by thus destroying its hypothesis, confirm
the proposition it set out to establish."
https://users.cecs.anu.edu.au/~jks/LogicNotes/RAA.html
This is also utter nonsense what John Slaney
writes, namely when he says:
"The result is that the rule RAA (Reductio ad absurdum) is
equivalent in the context of the rest of the natural
deduction system to the two rules ¬I and ¬E"
https://users.cecs.anu.edu.au/~jks/LogicNotes/RAA.html
Its not that RAA combines ~I and ~E. It combines
~I and DNE. Combining ~I and ~E is pointless. Nobody
would give it a new name. Already in DC Proof ~I
and ~E are combined, and it has the name of ~I. But
this nonsense is very common. You find it all over the
internet. Similar like you find funny cats on the
internet, you find RAA misrepresentations.
John Slaney is not RAA. Since it introduces a negation.
It goes from B to ~B. But for RAA you need to go from
~B to B, read Euclid below carefully!
X, B ⊢ A
Y, B ⊢ ¬A
---------------------- (Wrong Label RAA, should say ~Intro)
X, Y ⊢ ¬B
Figure 3.5.1.2
So maybe van Dalen should have written "Novice"
and "Grown Ups" make this error. That they cannot
distingish RAA from ~Intro.
Well, we don't live in a perfect world. This is a fast
paced world, where everybody can put any nonsense
on the internet. Even if he didn't understand Euclid:
"Every reduction to impossibility takes the contradictory
of what it intends to prove and from this as a hypothesis
proceeds until it encounters something admitted to be
absurd and, by thus destroying its hypothesis, confirm
the proposition it set out to establish."
https://users.cecs.anu.edu.au/~jks/LogicNotes/RAA.html
This is also utter nonsense what John Slaney
writes, namely when he says:
"The result is that the rule RAA (Reductio ad absurdum) is
equivalent in the context of the rest of the natural
deduction system to the two rules ¬I and ¬E"
https://users.cecs.anu.edu.au/~jks/LogicNotes/RAA.html
Its not that RAA combines ~I and ~E. It combines
~I and DNE. Combining ~I and ~E is pointless. Nobody
would give it a new name. Already in DC Proof ~I
and ~E are combined, and it has the name of ~I. But
this nonsense is very common. You find it all over the
internet. Similar like you find funny cats on the
internet, you find RAA misrepresentations.
Julio Di Egidio
Mar 21, 2023, 11:06:00 AM3/21/23
to
On Tuesday, 21 March 2023 at 15:45:33 UTC+1, Dan Christensen wrote:
> On Tuesday, March 21, 2023 at 10:23:14 AM UTC-4, Julio Di Egidio wrote:
> > On Tuesday, 21 March 2023 at 14:42:33 UTC+1, Dan Christensen wrote:
> > > On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
> > >
> > > > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > > > >
> > > > > > In school one should rather learn that there is nothing innocent about that.
> > > > >
> > > > > That would be a disservice to students.
> > > >
> > > > That is only a disservice to [snip childish abuse] you.
BTW, what you snip is a fairly precise characterization of the
> On Tuesday, March 21, 2023 at 10:23:14 AM UTC-4, Julio Di Egidio wrote:
> > On Tuesday, 21 March 2023 at 14:42:33 UTC+1, Dan Christensen wrote:
> > > On Tuesday, March 21, 2023 at 8:02:37 AM UTC-4, Julio Di Egidio wrote:
> > >
> > > > > > > Did you not learn basic logic in school, Mr. Collapse? If ~~P is true, then so is P. Maybe you slept through that lesson?
> > > > >
> > > > > > In school one should rather learn that there is nothing innocent about that.
> > > > >
> > > > > That would be a disservice to students.
> > > >
> > > > That is only a disservice to [snip childish abuse] you.
category in question, the you part is the less relevant one.
> > > Come now! You can play these games with consenting adults,
> [snip childish abuse]
> > > but would you really tell a 12-year-old that there is something
> > > ambiguous about the sentence, "It is false that it is not raining?"
>
> > Is simply trivial that [~R -> ~R], i.e. that "if you see that it is not
> > raining, then it is indeed not raining". But [~~R -> R] means that
> > "if you do not see that it is not raining, then you can conclude
> > that it is raining", which is altogether in another league...
>
> Nice bit of handwaving, Julio, but if you were being honest, you
> would tell the child that it means that it is indeed raining. There is
> nothing ambiguous about it.
asshole. LEM is of course fine over decidable types, and the
"raining" example is indeed a good example, of the fact that
accepting LEM unconditionally is *tacitly assuming that you can
and will unconditionally actually check whether it is raining or not*,
which is simply false in generally... which in turn means that such
a rule (DNE) would be logically acceptable iff you can and have in
fact checked whether it is raining or not, after which R is rather just
trivially either true or false, whichever it actually happens to be.
TL;DR Lying with logic: akin to "you cannot not communicate", or
"silence is admission", and similar abuses, not just of logic. DNE
does have its places, but one must know what it's doing, i.e. what
it's being tacitly assumed.
HTH and I am out of here.
Julio
Mostowski Collapse
Mar 21, 2023, 11:37:43 AM3/21/23
to
"ambiguous" is the wrong word for "constructive". Dan Christensen
uses always the wrond "ambiguous" where he thinks there is
a logical problem. But what does "ambiguous" have to do with
the logical problem of "constructivism"? Could you tell us?
uses always the wrond "ambiguous" where he thinks there is
a logical problem. But what does "ambiguous" have to do with
the logical problem of "constructivism"? Could you tell us?
Dan Christensen
Mar 21, 2023, 12:03:59 PM3/21/23
to
On Tuesday, March 21, 2023 at 11:06:00 AM UTC-4, Julio Di Egidio wrote:
[snip]
> > > > Come now! You can play these games with consenting adults,
> > Nice bit of handwaving, Julio, but if you were being honest, you
> > would tell the child that it means that it is indeed raining. There is
> > nothing ambiguous about it.
> That is NOT what it means [snip]
Oh, dear... We have a True Believer on our hands.
EOD
[snip]
> > > > Come now! You can play these games with consenting adults,
> > > > but would you really tell a 12-year-old that there is something
> > > > ambiguous about the sentence, "It is false that it is not raining?"
> >
> > > Is simply trivial that [~R -> ~R], i.e. that "if you see that it is not
> > > raining, then it is indeed not raining"
[snip more of the same]
> > > > ambiguous about the sentence, "It is false that it is not raining?"
> >
> > > Is simply trivial that [~R -> ~R], i.e. that "if you see that it is not
> > > raining, then it is indeed not raining"
> > Nice bit of handwaving, Julio, but if you were being honest, you
> > would tell the child that it means that it is indeed raining. There is
> > nothing ambiguous about it.
Oh, dear... We have a True Believer on our hands.
EOD
Mostowski Collapse
Mar 21, 2023, 2:07:10 PM3/21/23
to
But the web site does not have only open proofs. There are
also a couple of closed proofs. For example the web site
has the Drinker Paradox:
"Funny example
Let us take a non-empty bar. Give a proof in natural deduction
of the following sentence : "there exists a person such that, if
he/she drinks then everybody drinks". You may use the formula
P(x) to formalize the fact that the person denoted by x drinks."
http://pravda.irisa.fr/naturaldeduction.html
Can we replicate this proof in DC Poop? It uses absurd(3)
and absurd(14) and absurd(28). So I guess we cannot replicate
it directly in DC Poop.
also a couple of closed proofs. For example the web site
has the Drinker Paradox:
"Funny example
Let us take a non-empty bar. Give a proof in natural deduction
of the following sentence : "there exists a person such that, if
he/she drinks then everybody drinks". You may use the formula
P(x) to formalize the fact that the person denoted by x drinks."
http://pravda.irisa.fr/naturaldeduction.html
Can we replicate this proof in DC Poop? It uses absurd(3)
and absurd(14) and absurd(28). So I guess we cannot replicate
it directly in DC Poop.
Dan Christensen
Mar 21, 2023, 3:31:25 PM3/21/23
to
See my reply just now to your identical posting at sci.math
Dan
Dan
Mostowski Collapse
Mar 21, 2023, 4:34:14 PM3/21/23
to
I agree the proof here:
"Drinkers Paradox"
http://pravda.irisa.fr/naturaldeduction.html
is a big mess. I want to tidy it.
There are a few problems with the proof on pravda.irisa.fr:
- the MathJax needs a 2 meters wide screen
- the ASCII shows sequents with a lot of redundant premisses
On the other hand, I guess it has some advantage:
- it probably uses RAA and ~Intro, so its easier to see where
it is classical and where not, without boating the proof.
If you use DNE you get longer proofs (i.e. DC Poop)
- it uses probably easier quantifier rules than those
provided by other tools (i.e. DC Poop), that cannot prove this here:
6 p(a) -> ~ALL(x):~P(x)
Conclusion 1,5
"Drinkers Paradox"
http://pravda.irisa.fr/naturaldeduction.html
is a big mess. I want to tidy it.
There are a few problems with the proof on pravda.irisa.fr:
- the MathJax needs a 2 meters wide screen
- the ASCII shows sequents with a lot of redundant premisses
On the other hand, I guess it has some advantage:
- it probably uses RAA and ~Intro, so its easier to see where
it is classical and where not, without boating the proof.
If you use DNE you get longer proofs (i.e. DC Poop)
- it uses probably easier quantifier rules than those
provided by other tools (i.e. DC Poop), that cannot prove this here:
6 p(a) -> ~ALL(x):~P(x)
Conclusion 1,5
Dan Christensen
Mar 21, 2023, 5:14:12 PM3/21/23
to
See my reply just now to your identical posting at sci.math
Dan
Dan
Mostowski Collapse
Mar 21, 2023, 6:11:37 PM3/21/23
to
My RAA respectively DNE quest got a new spin.
How many RAA respectively DNE does a proof need?
It depends on how many quantifier it has.
If it doesn't have any quantifiers a single RAA
respectively DNE at the top-level should be enough.
Otherwise I find this note:
> The propositional mapping of φ to ¬¬φ does not
> extend to a sound translation of first-order logic,
> because the so called double negation shift
>
> ∀x ¬¬φ(x) → ¬¬∀x φ(x)
>
> is not a theorem of intuitionistic predicate logic. This
> explains why φN has to be defined in a more
> complicated way in the first-order case.
https://en.wikipedia.org/wiki/Double-negation_translation
Because the Drinker Paradox has quatifiers, it
can happen that it needs multiple RAAs respectively
DNE. What do we know about the constructivness
of the Drinker Paradox or the other quest, the Barber Paradox?
How many RAA respectively DNE does a proof need?
It depends on how many quantifier it has.
If it doesn't have any quantifiers a single RAA
respectively DNE at the top-level should be enough.
Otherwise I find this note:
> The propositional mapping of φ to ¬¬φ does not
> extend to a sound translation of first-order logic,
> because the so called double negation shift
>
> ∀x ¬¬φ(x) → ¬¬∀x φ(x)
>
> is not a theorem of intuitionistic predicate logic. This
> explains why φN has to be defined in a more
> complicated way in the first-order case.
https://en.wikipedia.org/wiki/Double-negation_translation
Because the Drinker Paradox has quatifiers, it
can happen that it needs multiple RAAs respectively
DNE. What do we know about the constructivness
of the Drinker Paradox or the other quest, the Barber Paradox?
Mostowski Collapse
Mar 21, 2023, 6:29:43 PM3/21/23
to
Can you show this formula:
((p->q)->p)->p
With only one RAA respectively DNE application at the top?
For example this proof is not of this kind, it has two Rem DNeg:
Proof 2: Using DNE
1 (p -> q) -> p
Premise
((p->q)->p)->p
With only one RAA respectively DNE application at the top?
For example this proof is not of this kind, it has two Rem DNeg:
Proof 2: Using DNE
1 (p -> q) -> p
Premise
2 ~p
Premise
3 p
Premise
4 ~q
Premise
Premise
3 p
Premise
4 ~q
Premise
5 ~p & p
Join 2,3
6 ~~q
Conclusion 4,5
7 q
Rem DNeg 6
8 p -> q
Conclusion 3,7
9 p
Detach 1,8
10 ~p & p
Join 2,9
11 ~~p
Conclusion 2,10
12 p
Rem DNeg 11
13 ((p -> q) -> p) -> p
Conclusion 1,12
Join 2,3
6 ~~q
Conclusion 4,5
7 q
Rem DNeg 6
8 p -> q
Conclusion 3,7
9 p
Detach 1,8
10 ~p & p
Join 2,9
11 ~~p
Conclusion 2,10
12 p
Rem DNeg 11
13 ((p -> q) -> p) -> p
Conclusion 1,12
Dan Christensen
Mar 21, 2023, 7:42:25 PM3/21/23
to
See my reply yesterday to your identical posting at sci.math
Dan
On Tuesday, March 21, 2023 at 6:29:43 PM UTC-4, Mostowski Collapse wrote:
> Can you show this formula:
>
> ((p->q)->p)->p
>
>[snip]
Dan
On Tuesday, March 21, 2023 at 6:29:43 PM UTC-4, Mostowski Collapse wrote:
> Can you show this formula:
>
> ((p->q)->p)->p
>
Mostowski Collapse
Mar 22, 2023, 4:57:07 PM3/22/23
to
Can you show a proof which has only DNE in the root,
this is the question. You didn't show such a proof yesterday.
It has DNE twice, and one is not in the root:
7 q
Rem DNeg 6
According to this theorem there should be a proof with
DNE in the root, when the theorem is a propositional formula:
"The easiest double-negation translation to describe
comes from Glivenko's theorem, proved by Valery Glivenko in 1929.
If φ is a propositional formula, then φ is a classical tautology if
and only if ¬¬φ is an intuitionistic tautology."
https://en.wikipedia.org/wiki/Double-negation_translation
Can you show a proof with DNE in the root, and no other DNE?
Can you do this via DC Poop? I doubt. There is something
missing in DC Poop, which makes this impossible.
this is the question. You didn't show such a proof yesterday.
It has DNE twice, and one is not in the root:
7 q
Rem DNeg 6
DNE in the root, when the theorem is a propositional formula:
"The easiest double-negation translation to describe
comes from Glivenko's theorem, proved by Valery Glivenko in 1929.
If φ is a propositional formula, then φ is a classical tautology if
and only if ¬¬φ is an intuitionistic tautology."
https://en.wikipedia.org/wiki/Double-negation_translation
Can you show a proof with DNE in the root, and no other DNE?
Can you do this via DC Poop? I doubt. There is something
missing in DC Poop, which makes this impossible.
Mostowski Collapse
Mar 26, 2023, 1:49:16 PM3/26/23
to
Lean Prover disagrees, it finds true and false perfectly
legitimate to be used. BTW, can you prove this drinker paradox:
EXIST(x):ALL(y):[p(x) v ~p(y)]
LMAO!
Dan Christensen schrieb am Donnerstag, 23. März 2023 um 03:41:19 UTC+1:
> As in proofs in most math textbooks, in DC Proof, there are no symbols for true
> and false to create confusion. They just aren't needed.
legitimate to be used. BTW, can you prove this drinker paradox:
EXIST(x):ALL(y):[p(x) v ~p(y)]
LMAO!
Dan Christensen schrieb am Donnerstag, 23. März 2023 um 03:41:19 UTC+1:
> As in proofs in most math textbooks, in DC Proof, there are no symbols for true
> and false to create confusion. They just aren't needed.
Dan Christensen
Mar 26, 2023, 5:15:02 PM3/26/23
to
On Sunday, March 26, 2023 at 1:49:16 PM UTC-4, Mostowski Collapse wrote:
> Lean Prover disagrees, it finds true and false perfectly
> legitimate to be used. BTW, can you prove this drinker paradox:
>
Sadly for you, these constants are not much used in math textbooks. Must be frustrating as hell for you, Mr. Collapse.
> Lean Prover disagrees, it finds true and false perfectly
> legitimate to be used. BTW, can you prove this drinker paradox:
>
Maybe you can take on Terry Tao and write a textbook on real analysis using your wonky ideas on logic and set theory.
Mostowski Collapse
Mar 27, 2023, 3:23:51 PM3/27/23
to
You sure about your claim? It would be rather sad if you
claim is wrong, isn't it? Making you the super crank you are.
Worse than WM and John Gabriel together. So you
never saw in a math book somebody writing:
quod patet esse falsum
[which is obviously false]
LoL
claim is wrong, isn't it? Making you the super crank you are.
Worse than WM and John Gabriel together. So you
never saw in a math book somebody writing:
quod patet esse falsum
[which is obviously false]
LoL
Dan Christensen
Mar 27, 2023, 4:09:45 PM3/27/23
to
On Monday, March 27, 2023 at 3:23:51 PM UTC-4, Mostowski Collapse wrote:
> Dan Christensen schrieb am Sonntag, 26. März 2023 um 23:15:02 UTC+2:
> > On Sunday, March 26, 2023 at 1:49:16 PM UTC-4, Mostowski Collapse wrote:
> > > Lean Prover disagrees, it finds true and false perfectly
> > > legitimate to be used. BTW, can you prove this drinker paradox:
> > >
> > Sadly for you, these constants are not much used in math textbooks. Must be frustrating as hell for you, Mr. Collapse.
> >
> > Maybe you can take on Terry Tao and write a textbook on real analysis using your wonky ideas on logic and set theory.
> Dan Christensen schrieb am Sonntag, 26. März 2023 um 23:15:02 UTC+2:
> > On Sunday, March 26, 2023 at 1:49:16 PM UTC-4, Mostowski Collapse wrote:
> > > Lean Prover disagrees, it finds true and false perfectly
> > > legitimate to be used. BTW, can you prove this drinker paradox:
> > >
> > Sadly for you, these constants are not much used in math textbooks. Must be frustrating as hell for you, Mr. Collapse.
> >
> > Maybe you can take on Terry Tao and write a textbook on real analysis using your wonky ideas on logic and set theory.
> You sure about your claim?
Yup. Not used in proofs.
Dan
Mostowski Collapse
Mar 27, 2023, 8:59:11 PM3/27/23
to
Well I see it used in proofs all the time, do you
deny that there is a falsum on the right hand side,
for all rows of this truth table:
P (P ∧ ¬P)
F F
T F
https://web.stanford.edu/class/cs103/tools/truth-table-tool/
What does F mean? What does the phrase mean, that
a formula and its negation form a contradiction? Its nothing
else than this falsum introduction rule:
G |- A G |- ~A
------------------------------ (f-Intro)
G |- f
Only you don't have it in DC Poop, since DC Poop is
a little minimalistic.
deny that there is a falsum on the right hand side,
for all rows of this truth table:
P (P ∧ ¬P)
F F
T F
https://web.stanford.edu/class/cs103/tools/truth-table-tool/
What does F mean? What does the phrase mean, that
a formula and its negation form a contradiction? Its nothing
else than this falsum introduction rule:
G |- A G |- ~A
------------------------------ (f-Intro)
G |- f
Only you don't have it in DC Poop, since DC Poop is
a little minimalistic.
Mostowski Collapse
Mar 27, 2023, 9:02:06 PM3/27/23
to
Woa! Even the stanford truth table generator
allows falsum () in the formula input. Something
DC Poop can only dream of:
P (P ∧ (P → ⊥))
You cannot prove (P ∧ (P → ⊥)) → ⊥ in DC Poop
right? Because DC Poop is for squirells and not for
mathematics? Its very minimalistic, and has no
room for verum (⊤) and falsum (⊥).
LMAO!
allows falsum () in the formula input. Something
DC Poop can only dream of:
P (P ∧ (P → ⊥))
You cannot prove (P ∧ (P → ⊥)) → ⊥ in DC Poop
right? Because DC Poop is for squirells and not for
mathematics? Its very minimalistic, and has no
room for verum (⊤) and falsum (⊥).
LMAO!
0 new messages