The principle of explosion diverges from correct reasoning

[olcott]

*Principle of explosion*
https://en.wikipedia.org/wiki/Principle_of_explosion#Proof

<quote>
In symbolic logic, the principle of explosion can be expressed
schematically in the following way:

P, ¬P ⊢ Q For any statements P and Q, if P and not-P are both true, then
it logically follows that Q is true.

*Step --- Proposition --- Derivation*
1 -------- P ------------ Assumption
2 ------- ¬P ------------ Assumption
3 -------- P ∨ Q -------- Disjunction introduction (1)
4 -------- Q ------------ Disjunctive syllogism (3,2)
</quote>

*Truth table for P ∧ ¬P*
P----¬P----P ∧ ¬P
T-----F------F
F-----T------F

With arithmetic we know that we must perform the operations in a
specific order or we get the wrong answer. (2 * 3) + (4 * 5) = (6 + 20)
We resolve the inner operations before proceeding. If we don't do this
same thing in logic we get absurd results.

When the text says P, ¬P ⊢ Q it failed to resolve P ∧ ¬P ⊢ False
before moving to the next step. This is a key aspect of the absurd
results. It is not a logic error. It is the divergence of logic from
correct reasoning. When two premises contradict each other (in correct
reasoning) this resolves to false.

When we resolve P ∨ ¬P to False then it becomes clear that Disjunction
introduction cannot be performed (False ∨ Q) ⊢ Q transforms the unknown
truth value of Q to true.

--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[Dan Christensen]

A more straightforward proof:

1. P & ~P
Premise

2. ~Q
Premise

3. P & ~P
Copy, 1

4. ~~Q
Conclusion, 2

5. Q
Rem DNeg, 4

6. P & ~P => Q
Conclusion, 1

Which step do suppose is invalid? The proof by contradiction on (4)? Removal of ~~ on (5)? Conditional proof on (6)?

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Richard Damon]

On 5/21/23 10:52 PM, olcott wrote:
> *Principle of explosion*
> https://en.wikipedia.org/wiki/Principle_of_explosion#Proof
>
> <quote>
> In symbolic logic, the principle of explosion can be expressed
> schematically in the following way:
>
> P, ¬P ⊢ Q For any statements P and Q, if P and not-P are both true, then
> it logically follows that Q is true.
>
> *Step --- Proposition --- Derivation*
> 1 -------- P ------------ Assumption

Not really an "Assumption", but a proven given.

The problem with working with oversimpified explanations.

> 2 ------- ¬P ------------ Assumption

Not really an "Assumption", but a proven given.

> 3 -------- P ∨ Q -------- Disjunction introduction (1)
> 4 -------- Q ------------ Disjunctive syllogism (3,2)
> </quote>
>
> *Truth table for P ∧ ¬P*
> P----¬P----P ∧ ¬P
> T-----F------F
> F-----T------F

So?

There is no requirement to check a given resul with all rules defined in
the system.

>
> With arithmetic we know that we must perform the operations in a
> specific order or we get the wrong answer. (2 * 3) + (4 * 5) = (6 + 20)
> We resolve the inner operations before proceeding. If we don't do this
> same thing in logic we get absurd results.
>
> When the text says P, ¬P ⊢ Q it failed to resolve P ∧ ¬P ⊢ False

Where is that statement in the expression?

Also, we know that True ∧ ¬True ⊢ True,

So which rule gets priority.


Note, it is the "Assumptions" that "violate" the rule, so the
assumptions are the source of the issue.

> before moving to the next step. This is a key aspect of the absurd
> results. It is not a logic error. It is the divergence of logic from
> correct reasoning. When two premises contradict each other (in correct
> reasoning) this resolves to false.

No, it is the divergance of the assumptions from correct logic. The key
is that the principle of explosion points out that if we can prove a
contradiction, our system has inconsistent givens.

>
> When we resolve P ∨ ¬P to False then it becomes clear that Disjunction
> introduction cannot be performed (False ∨ Q) ⊢ Q transforms the unknown
> truth value of Q to true.
>

It isn't that the principle of eplosion diverges from correct reasoning,
the principle of explosion just points out that a system that has
allowed the proving of a contradiction has deviated from "Correctness"
by the fact that it can prove a contradiction, and a system that can
prove one contradiction can prove many.

You are just showing how little you understand how logic works.

[Richard Damon]

As an addition, since it is your adding the assumption that H can call
an input non-halting just because it determines that no variation of H
can correctly simulate that input to a final state, and this rules leads
us to being able to actually prove that D(D) is both Halting (by running
it) and Non-Halting (by asking H) says that you added assumption makes
the system inconsistent, and thus your assumption is a violation of
correct reasoning.

[olcott]

On 5/22/2023 6:49 AM, Richard Damon wrote:
> On 5/21/23 10:52 PM, olcott wrote:
>> *Principle of explosion*
>> https://en.wikipedia.org/wiki/Principle_of_explosion#Proof
>>
>> <quote>
>> In symbolic logic, the principle of explosion can be expressed
>> schematically in the following way:
>>
>> P, ¬P ⊢ Q For any statements P and Q, if P and not-P are both true,
>> then it logically follows that Q is true.
>>
>> *Step --- Proposition --- Derivation*
>> 1 -------- P ------------ Assumption
>
> Not really an "Assumption", but a proven given.
>

So you don't understand that the premises to a proof are only
assumptions? A proof is always based on the hypothetical assumption that
its premises are true. The intent is to see if a conclusion can be drawn
by applying truth preserving operations to these premises. If this is
the case then we know that the conclusion logically follows from its
premises, we don't know that the conclusion is true unless it is also
stipulated that the premises are true.

> The problem with working with oversimpified explanations.
>
>> 2 ------- ¬P ------------ Assumption
>
>
> Not really an "Assumption", but a proven given.
>
>> 3 -------- P ∨ Q -------- Disjunction introduction (1)
>> 4 -------- Q ------------ Disjunctive syllogism (3,2)
>> </quote>
>>
>> *Truth table for P ∧ ¬P*
>> P----¬P----P ∧ ¬P
>> T-----F------F
>> F-----T------F
>
> So?
>
> There is no requirement to check a given resul with all rules defined in
> the system.
>
>>
>> With arithmetic we know that we must perform the operations in a
>> specific order or we get the wrong answer. (2 * 3) + (4 * 5) = (6 + 20)
>> We resolve the inner operations before proceeding. If we don't do this
>> same thing in logic we get absurd results.
>>
>> When the text says P, ¬P ⊢ Q it failed to resolve P ∧ ¬P ⊢ False
>
> Where is that statement in the expression?
>

I am saying that by not first resolving P ∧ ¬P to false according to
the truth table of P ∧ ¬P an absurd conclusion is drawn. This is where
logic diverges from correct reasoning.

> Also, we know that True ∧ ¬True ⊢ True,
>

We are not dealing with True ∧ ¬True.
We are dealing with P ∧ ¬P ⊢ False.

> So which rule gets priority.
>
>
> Note, it is the "Assumptions" that "violate" the rule, so the
> assumptions are the source of the issue.
>

Easily resolved when P ∧ ¬P ⊢ False is resolved before proceeding.

>> before moving to the next step. This is a key aspect of the absurd
>> results. It is not a logic error. It is the divergence of logic from
>> correct reasoning. When two premises contradict each other (in correct
>> reasoning) this resolves to false.
>
> No, it is the divergance of the assumptions from correct logic. The key
> is that the principle of explosion points out that if we can prove a
> contradiction, our system has inconsistent givens.
>

Yet we cannot prove a contradiction when when P ∧ ¬P ⊢ False is
resolved before proceeding.

>>
>> When we resolve P ∨ ¬P to False then it becomes clear that Disjunction
>> introduction cannot be performed (False ∨ Q) ⊢ Q transforms the unknown
>> truth value of Q to true.
>>
>
> It isn't that the principle of eplosion diverges from correct reasoning,
> the principle of explosion just points out that a system that has
> allowed the proving of a contradiction has deviated from "Correctness"
> by the fact that it can prove a contradiction, and a system that can
> prove one contradiction can prove many.
>
> You are just showing how little you understand how logic works.
>

I am showing how little logic knows about correct reasoning.
We know from its truth table that P ∧ ¬P ⊢ False, thus the
short-circuit that proves a contradiction violates the truth
table of P ∧ ¬P.

We also know that Disjunction introduction to False breaks the
truth preserving requirements by transforming the unknown truth

value of Q to true.

[Richard Damon]

On 5/22/23 10:12 AM, olcott wrote:
> On 5/22/2023 6:49 AM, Richard Damon wrote:
>> On 5/21/23 10:52 PM, olcott wrote:
>>> *Principle of explosion*
>>> https://en.wikipedia.org/wiki/Principle_of_explosion#Proof
>>>
>>> <quote>
>>> In symbolic logic, the principle of explosion can be expressed
>>> schematically in the following way:
>>>
>>> P, ¬P ⊢ Q For any statements P and Q, if P and not-P are both true,
>>> then it logically follows that Q is true.
>>>
>>> *Step --- Proposition --- Derivation*
>>> 1 -------- P ------------ Assumption
>>
>> Not really an "Assumption", but a proven given.
>>
>
> So you don't understand that the premises to a proof are only
> assumptions? A proof is always based on the hypothetical assumption that
> its premises are true. The intent is to see if a conclusion can be drawn
> by applying truth preserving operations to these premises. If this is
> the case then we know that the conclusion logically follows from its
> premises, we don't know that the conclusion is true unless it is also
> stipulated that the premises are true.

No, most of the times, they are proven statements in the system. Yes,
you can start a proof starting with assuptions and get an answer that is
conditional on the assumption being true, but most of the time, your
input premises are known to be true, so you aren't working on a possible
dead end.

For the principle of explosion, they are statements of pre-condition,
the principle of explosion only applies *IF* you can establish that
there is some condition P, such that you can show that P and ~P are both
true.

Thus, they are "assumptions", but pre-conditions for the results.

Yes, you perform the operations of the proof starting with them as
"assumptions", but then they become the pre-condition of the theory, and
to be applied, they must be proven facts.

>
>> The problem with working with oversimpified explanations.
>>
>>> 2 ------- ¬P ------------ Assumption
>>
>>
>> Not really an "Assumption", but a proven given.
>>
>>> 3 -------- P ∨ Q -------- Disjunction introduction (1)
>>> 4 -------- Q ------------ Disjunctive syllogism (3,2)
>>> </quote>
>>>
>>> *Truth table for P ∧ ¬P*
>>> P----¬P----P ∧ ¬P
>>> T-----F------F
>>> F-----T------F
>>
>> So?
>>
>> There is no requirement to check a given resul with all rules defined
>> in the system.
>>
>>>
>>> With arithmetic we know that we must perform the operations in a
>>> specific order or we get the wrong answer. (2 * 3) + (4 * 5) = (6 + 20)
>>> We resolve the inner operations before proceeding. If we don't do this
>>> same thing in logic we get absurd results.
>>>
>>> When the text says P, ¬P ⊢ Q it failed to resolve P ∧ ¬P ⊢ False
>>
>> Where is that statement in the expression?
>>
>
> I am saying that by not first resolving P ∧ ¬P to false according to
> the truth table of P ∧ ¬P an absurd conclusion is drawn. This is where
> logic diverges from correct reasoning.

So, do you check ALL your premises to ALL other possible rules?

If so, why don't you see that H must be wrong, because even without
doing your argument about what any H can do, since we have the
definition of your H, and it is establish fact, just by running it, that
H(D,D) returns 0, and it is established fact that by running D(D) it
Halts, that H must be returning the wrong answer, since that is what it
is supposed to be answering.

ANSWER: You haven't check the established rules, and thus don't see that
your "assumption" that H can answer non-halting because no H can
simulate its input to a final state leads to an inconsistant logic system.

>
>> Also, we know that True ∧ ¬True ⊢ True,
>>
>
> We are not dealing with True ∧ ¬True.
> We are dealing with P ∧ ¬P ⊢ False.

No, we are dealing with a logic arguement that begins:

Assume P,
Assume ¬P

Therefore, when we evaluate P ∧ ¬P we know the values and can substitute
them in. And thus your rule becomes True ⊢ False

In fact, once we have the two assumptions, we can show the system in
inconsistant, and the principle of explosion is just showing the
possible effect of that.

>
>> So which rule gets priority.
>>
>>
>> Note, it is the "Assumptions" that "violate" the rule, so the
>> assumptions are the source of the issue.
>>
>
> Easily resolved when P ∧ ¬P ⊢ False is resolved before proceeding.

But you don't need to do that, and in fact, it is superfluous, as the
definition of NOT is defied already.

>
>>> before moving to the next step. This is a key aspect of the absurd
>>> results. It is not a logic error. It is the divergence of logic from
>>> correct reasoning. When two premises contradict each other (in correct
>>> reasoning) this resolves to false.
>>
>> No, it is the divergance of the assumptions from correct logic. The
>> key is that the principle of explosion points out that if we can prove
>> a contradiction, our system has inconsistent givens.
>>
>
> Yet we cannot prove a contradiction when when P ∧ ¬P ⊢ False is
> resolved before proceeding.

So, you don't understand how logic works, proving your ignorance.

We HAD the contradition once we had P and ~P as premises.

>
>>>
>>> When we resolve P ∨ ¬P to False then it becomes clear that Disjunction
>>> introduction cannot be performed (False ∨ Q) ⊢ Q transforms the unknown
>>> truth value of Q to true.
>>>
>>
>> It isn't that the principle of eplosion diverges from correct
>> reasoning, the principle of explosion just points out that a system
>> that has allowed the proving of a contradiction has deviated from
>> "Correctness" by the fact that it can prove a contradiction, and a
>> system that can prove one contradiction can prove many.
>>
>> You are just showing how little you understand how logic works.
>>
>
> I am showing how little logic knows about correct reasoning.
> We know from its truth table that P ∧ ¬P ⊢ False, thus the
> short-circuit that proves a contradiction violates the truth
> table of P ∧ ¬P.

No, you are showing how little you know about logic.

You concept of "Correct Reasoning" seems doomed to failure because it
doesn't understand how logic works.

>
> We also know that Disjunction introduction to False breaks the
> truth preserving requirements by transforming the unknown truth
> value of Q to true.
>

So, if A and B are know Truth Bearers, and A ∨ B is proven to be a True
expression, and then A is proven to be False, what is B?

[olcott]

Do You know the Mendelson Text?
According to Mendelson only theorems have premises known to be true.

> For the principle of explosion, they are statements of pre-condition,
> the principle of explosion only applies *IF* you can establish that
> there is some condition P, such that you can show that P and ~P are both
> true.
>

That is the same thing as saying if horses were office buildings then
you could wash their windows.

It is a truism that when you assume contradictory premises that they
only derive False. When you try this semantically it is obvious.

[Richard Damon]

Right, or CONDITIONS under which they hold. For instance, Godel's
incompleteness proof only holds for systems that support the needed
properties of the Natural Numbers, and which are consistant.

The principle of Explosion holds for system that system that support the
Disjunctive Syllogism (or some other similar operations) AND can prove
two contradictory premises.

>
>> For the principle of explosion, they are statements of pre-condition,
>> the principle of explosion only applies *IF* you can establish that
>> there is some condition P, such that you can show that P and ~P are
>> both true.
>>
>
> That is the same thing as saying if horses were office buildings then
> you could wash their windows.
>

You would first need some axioms that establish that horses have windows.

Note, "Formal Systems" don't need to model the physical universe.

Remember, if wishes were horses then beggars would ride.

> It is a truism that when you assume contradictory premises that they
> only derive False. When you try this semantically it is obvious.
>

Right, but the principle of explosion isn't based on ASSUMING
contradictory premises, but on being able to PROVE contradictory
premises, which is an indication that you axioms are inconsistent.

Like it appears your "Correct Reasoning" is, as somehow it seems to be
saying that a Halting Computation can be corrected described as
Non-Halting, amoung other contradictions.

[olcott]

So assuming that P ∧ ¬P ⊢ True (which it does not) then the principle
of explosion is entailed.

"That is to say, the principle of explosion is an argument for the law
of non-contradiction in classical logic, because without it all truth
statements become meaningless."

We already knew that the law of of non-contradiction is necessarily true
so the POE is redundant.

So the POE has always only been a hypothetical argument to prove the law
of of non-contradiction. That makes sense.

[Richard Damon]

Sort of, you don't seem to understand that logical terms:

The PRECONDITION to use the Principle of Explosion is that a system can
establish both P and ¬P. You can't say that it can't happen, because
people playing with system accedentally create conditions that allow
such a statement to be proven.

>
> "That is to say, the principle of explosion is an argument for the law
> of non-contradiction in classical logic, because without it all truth
> statements become meaningless."

The Principle of Explosion shows that a classical logic system can not
allow a contradiction, as if it does, it makes truth within the system

meaningless.

>
> We already knew that the law of of non-contradiction is necessarily true
> so the POE is redundant.

No, it shows the effect of violating the "law of non-contradiction".

>
> So the POE has always only been a hypothetical argument to prove the law
> of of non-contradiction. That makes sense.
>

It isn't just hypothetical, because systems exist that violate the "lot
of non-contradiction", and it explains why we need to discard such
systems, like yours.

[olcott]

All these years I thought that it was being asserted that the POE is
true and that everything is actually proven from a contradiction.

All the time they were never saying that, they were only saying what
happens when we hypothetically assume that a contradiction is true.

[Ross Finlayson]

The "material implication" is the same sort of garbage as the falso
that the 'ex falso quod falso' results.

Two wrongs do _not_ make a right.

Of course that's not to be confused with the dialectic and critical reasoning about
limits meeting in the middle of what, to induction, is nowhere.

[olcott]

I agree. It deceptively looks like if-then.

P Q If P then Q
T T T
T F F
F T ? can't be determined
F F ? can't be determined

> Two wrongs do _not_ make a right.
>
> Of course that's not to be confused with the dialectic and critical reasoning about
> limits meeting in the middle of what, to induction, is nowhere.
>

[Richard Damon]

You do understand that a proof can only happen from a true premise?

The principle of explosion says that if you ACTUALLY HAVE a
contradiction that is proven in the system, that the system blows up.

I guess this shows who little you understand of how logic actually works.

If you just "assume" a contradiction to be true, yes, you can prove that
based on that assumption, you can show anything true, but that is preety
worthless, as we should know the contradiction isn't true.

The issue is what happens when you find a contradiction in a logic
system, and why you really need to trace back and find what assumption /
axiom in the system causes that to be able to be proven.

For instance, this is what happened to naive set theory, and the work
done to remove the problem by changing fundamental rules on how you can
define sets.

[olcott]

On 5/21/2023 9:52 PM, olcott wrote:

All of these years I simply relied on a bad source, here is what the
Principle of Explosion really is

The principle of explosion is a logical rule of inference. According to
the rule, from a set of premises in which a sentence A and its negation
¬A are both true (i.e., a contradiction is true), any sentence B may be
inferred. https://rationalwiki.org/wiki/Principle_of_explosion

[Dan Christensen]

On Monday, May 22, 2023 at 11:14:29 PM UTC-4, Richard Damon wrote:

[snip]

> You do understand that a proof can only happen from a true premise?
>

Proofs do not necessarily start with a premise that is already known to be always true. They usually start with a provisional, what-if statement.

> The principle of explosion says that if you ACTUALLY HAVE a
> contradiction that is proven in the system, that the system blows up.
>
> I guess this shows who little you understand of how logic actually works.
>
> If you just "assume" a contradiction to be true, yes, you can prove that

> based on that assumption, you can show anything true.

[snip]

In my proof here, I started with the provisional, what if P & ~P was true? I concluded that P & ~P => Q. This result tells us nothing about the truth value of Q. It is actually indeterminate. It is the implication, not the consequent that is shown to be true here.

> For instance, this is what happened to naive set theory, and the work
> done to remove the problem by changing fundamental rules on how you can
> define sets.

There is no formal definition of the form "X is a set iff _______." There is apparently no need for one. However you might define a set, that definition would seldom, if ever, be required in a mathematical proof.

[olcott]

On 5/22/2023 10:56 PM, Dan Christensen wrote:
> On Monday, May 22, 2023 at 11:14:29 PM UTC-4, Richard Damon wrote:
>
> [snip]
>
>> You do understand that a proof can only happen from a true premise?
>>
>
> Proofs do not necessarily start with a premise that is already known to be always true. They usually start with a provisional, what-if statement.
>
>> The principle of explosion says that if you ACTUALLY HAVE a
>> contradiction that is proven in the system, that the system blows up.
>>
>> I guess this shows who little you understand of how logic actually works.
>>
>> If you just "assume" a contradiction to be true, yes, you can prove that
>> based on that assumption, you can show anything true.
>
> [snip]
>
> In my proof here, I started with the provisional, what if P & ~P was true?

All of these years I simply relied on a bad source, here is what the
Principle of Explosion really is

The principle of explosion is a logical rule of inference. According to
the rule, from a set of premises in which a sentence A and its negation
¬A are both true (i.e., a contradiction is true), any sentence B may be
inferred. https://rationalwiki.org/wiki/Principle_of_explosion

> I concluded that P & ~P => Q. This result tells us nothing about the truth value of Q. It is actually indeterminate. It is the implication, not the consequent that is shown to be true here.
>
>> For instance, this is what happened to naive set theory, and the work
>> done to remove the problem by changing fundamental rules on how you can
>> define sets.
>
> There is no formal definition of the form "X is a set iff _______." There is apparently no need for one. However you might define a set, that definition would seldom, if ever, be required in a mathematical proof.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

On Tuesday, May 23, 2023 at 12:07:41 AM UTC-4, olcott wrote:

[snip]

> > In my proof here, I started with the provisional, what if P & ~P was true?
> All of these years I simply relied on a bad source, here is what the
> Principle of Explosion really is
>
> The principle of explosion is a logical rule of inference. According to
> the rule, from a set of premises in which a sentence A and its negation
> ¬A are both true (i.e., a contradiction is true), any sentence B may be
> inferred.

Again, when I formally prove that the implication P & ~P => Q is true, I cannot infer anything about the truth value of Q. It is actually indeterminate. Logically, it could consistently be either true or false. Note that a proof is incomplete if every premise has not been discharge.

That proof again...

1. P & ~P
Premise

2. ~Q
Premise

3. P & ~P
Copy, 1

Here, the premise on line 2 has been discharged using the Conclusion Rule:

4. ~~Q
Conclusion, 2

5. Q
Rem DNeg, 4

Here, the premise on line 1 has yet to be discharged. As such, stopping here would leave the proof incomplete. To complete this proof, we need one more line that will discharge that remaining premise.

6. P & ~P => Q
Conclusion, 1

I hope this helps.

[Richard Damon]

On 5/22/23 11:18 PM, olcott wrote:
> On 5/21/2023 9:52 PM, olcott wrote:
>
> All of these years I simply relied on a bad source, here is what the
> Principle of Explosion really is
>
> The principle of explosion is a logical rule of inference. According to
> the rule, from a set of premises in which a sentence A and its negation
> ¬A are both true (i.e., a contradiction is true), any sentence B may be
> inferred. https://rationalwiki.org/wiki/Principle_of_explosion
>
>

So, the idiot can learn something.

MAybe some day you will come to a similar realization about all the
other things you think you know.

[olcott]

https://en.wikipedia.org/wiki/Principle_of_explosion

*Truth table for P ∧ ¬P*
P----¬P----P ∧ ¬P
T-----F------F
F-----T------F

Thus when the text says P, ¬P ⊢ Q it forgot to resolve P ∧ ¬P ⊢ False

*Step --- Proposition --- Derivation*
1 -------- P ------------ Assumption

2 ------- ¬P ------------ Assumption

3 -------- P ∨ Q -------- Disjunction introduction (1)
4 -------- Q ------------ Disjunctive syllogism (3,2)

The correct way to do this is P ∧ ¬P ⊢ False
then there no longer is any P for Disjunction introduction.

[Dan Christensen]

On Tuesday, May 23, 2023 at 9:34:52 AM UTC-4, olcott wrote:
> On 5/22/2023 11:52 PM, Dan Christensen wrote:

[snip]

> >> The principle of explosion is a logical rule of inference. According to
> >> the rule, from a set of premises in which a sentence A and its negation
> >> ¬A are both true (i.e., a contradiction is true), any sentence B may be
> >> inferred.
> >
> > Again, when I formally prove that the implication P & ~P => Q is true, I cannot infer anything about the truth value of Q. It is actually indeterminate. Logically, it could consistently be either true or false. Note that a proof is incomplete if every premise has not been discharge.
> >
> > That proof again...
> >
> > 1. P & ~P
> > Premise
> >
> > 2. ~Q
> > Premise
> >
> > 3. P & ~P
> > Copy, 1
> >
> > Here, the premise on line 2 has been discharged using the Conclusion Rule:
> >
> > 4. ~~Q
> > Conclusion, 2
> >
> > 5. Q
> > Rem DNeg, 4
> >
> > Here, the premise on line 1 has yet to be discharged. As such, stopping here would leave the proof incomplete. To complete this proof, we need one more line that will discharge that remaining premise.
> >
> > 6. P & ~P => Q
> > Conclusion, 1
> >

[snip]

> https://en.wikipedia.org/wiki/Principle_of_explosion
> *Truth table for P ∧ ¬P*
> P----¬P----P ∧ ¬P
> T-----F------F
> F-----T------F
> Thus when the text says P, ¬P ⊢ Q it forgot to resolve P ∧ ¬P ⊢ False
> *Step --- Proposition --- Derivation*
> 1 -------- P ------------ Assumption
> 2 ------- ¬P ------------ Assumption
> 3 -------- P ∨ Q -------- Disjunction introduction (1)
> 4 -------- Q ------------ Disjunctive syllogism (3,2)

[snip]

You forgot to discharge the assumptions/premises on lines 1 and 2. Doing so, you would conclude that P => (~P => Q) (a tautology) and that the truth value of Q would be indeterminate.

[olcott]

I am just quoting the Wikipedia article.
I would do this
(a) P ∧ ¬P ⊢ False
(b) False ⊬ Q

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Ross Finlayson]

OR, it establishes the theory is incomplete, as "DeMorgan, Boolean closed,
LEM, TND". (That there are other true theorems about the objects,
disambiguating what that "A or not A" is just ambiguity.)

At any rate it shows "more disambiguation needs result" that otherwise
"the logic of ambiguity is that there is not one".

[Dan Christensen]

On Tuesday, May 23, 2023 at 11:35:44 AM UTC-4, olcott wrote:

[snip]

> > You forgot to discharge the assumptions/premises on lines 1 and 2. [So did the Wikipedia article!] Doing so, you would conclude that P => (~P => Q) (a tautology) and that the truth value of Q would be indeterminate.

> >
> I am just quoting the Wikipedia article.
> I would do this
> (a) P ∧ ¬P ⊢ False
> (b) False ⊬ Q

Just finish your proof by discharging your assumptions/premises on lines 1 and 2 above, and get back to us. Or can you not discharge assumptions in your system??? Yikes!!

[olcott]

I just did discharge the assumptions on (a) above: P ∧ ¬P ⊢ False
Then I concluded that False ⊬ Q on 9a) above.

P assumption
¬P assumption
{P, ¬P} ≡ P ∧ ¬P conversion
----------------------------
P ∧ ¬P ⊢ False resolution

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

5 --------- ~P => Q ----------------- Discharge Assumption (2)
6 --------- P => (~P => Q) ------- Discharge Assumption (1)

End of Proof

> >>>
> >>> [snip]
> >>>
> >>> You forgot to discharge the assumptions/premises on lines 1 and 2. [So did the Wikipedia article!] Doing so, you would conclude that P => (~P => Q) (a tautology) and that the truth value of Q would be indeterminate.
> >>>
> >> I am just quoting the Wikipedia article.
> >> I would do this
> >> (a) P ∧ ¬P ⊢ False
> >> (b) False ⊬ Q
> >
> > Just finish your proof by discharging your assumptions/premises on lines 1 and 2 above, and get back to us. Or can you not discharge assumptions in your system??? Yikes!!
> >
> I just did discharge the assumptions on (a) above: P ∧ ¬P ⊢ False

Makes no sense.

> Then I concluded that False ⊬ Q on 9a) above.
>
> P assumption
> ¬P assumption
> {P, ¬P} ≡ P ∧ ¬P conversion
> ----------------------------
> P ∧ ¬P ⊢ False resolution

See my suggestion above. Questions?

[olcott]

Your statement seems to indicate that you don't understand (or accept)
the truth table of "and". I know that this interpretation can't be true
yet I see no other possible interpretation.

>> Then I concluded that False ⊬ Q on 9a) above.
>>
>> P assumption
>> ¬P assumption
>> {P, ¬P} ≡ P ∧ ¬P conversion
>> ----------------------------
>> P ∧ ¬P ⊢ False resolution
>
> See my suggestion above. Questions?
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[olcott]

⊥ F falsum, falsity
https://en.wikipedia.org/wiki/List_of_logic_symbols

(¬E) φ, ¬φ ⊢ ⊥ // contradictory premises resolve to falsum/false
https://iep.utm.edu/natural-deduction/#H4

Alternatively using the truth table for "and"

P----¬P----P ∧ ¬P
T-----F------F
F-----T------F

Your statement seems to indicate that you don't understand (or accept)
the truth table of "and". I know that this interpretation can't be true
yet I see no other possible interpretation.

>

>> Then I concluded that False ⊬ Q on 9a) above.
>>
>> P assumption
>> ¬P assumption
>> {P, ¬P} ≡ P ∧ ¬P conversion
>> ----------------------------
>> P ∧ ¬P ⊢ False resolution
>
> See my suggestion above. Questions?
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

On Tuesday, May 23, 2023 at 2:44:59 PM UTC-4, olcott wrote:

[snip]

[snip]

Your truth table, though correct, is irrelevant to this discussion. You clearly don't under basic methods of proof including the discharging of every premise/assumption that is required in any proof.

[olcott]

The letters I and E in the names of the rules come
from “introduction” and “elimination” respectively
since the first allows introduction of a conjunction
into a proof, and the second allows for its elimination
in favor of simpler formulas.

(¬E) φ, ¬φ ⊢ ⊥ // contradictory premises resolve to falsum/false
https://iep.utm.edu/natural-deduction/#H4

>

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com

[Dan Christensen]

Now look up how to discharge a premise/assumption to finish your proof. Then get back to us.

BTW the falsum symbol ⊥ is rarely if ever used in mathematical proofs. Try to avoid to its use. It really isn't necessary.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com

[olcott]

I already did discharge the premises when I converted P ∧ ¬P to False.
Terms of the art that override and supersede conventional meanings
are a generally bad communication practice that leads many astray.

https://www.dictionary.com/browse/discharge
to relieve of a charge or load; unload:

Paraphrase: get rid of.

I looked at several sites that tried to explain the term of the art and
it never made any sense.

https://mathoverflow.net/questions/3920/what-does-it-mean-to-discharge-assumptions-or-premises

https://users.cecs.anu.edu.au/~jks/LogicNotes/glossary/g_discharge.html

https://math.stackexchange.com/questions/3527285/what-does-discharging-an-assumption-mean-in-natural-deduction


https://sites.oxy.edu/traiger/logic/primer/chapter6/conditional-proof.html

> BTW the falsum symbol ⊥ is rarely if ever used in mathematical proofs. Try to avoid to its use. It really isn't necessary.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

Not very useful, I'm afraid.

Better is P & ~P => Q. It actually makes sense.

Better still is P => [~P => Q] (the principle of vacuous truth) which is quite useful in proofs.

Learn from my proofs here. This proof has 2 examples of discharging a premise using the Conclusion Rule on lines 4 and 6 .

1. P & ~P
Premise

2. ~Q
Premise

3. P & ~P
Copy, 1

Proof by contradiction:

4. ~~Q
Conclusion, 2

5. Q
Rem DNeg, 4

Conditional proof:

6. P & ~P => Q
Conclusion, 1

A variation discharging each premise using the Conclusion Rule on lines 5, 7 and 8:

1 P
Premise

2 ~P
Premise

3 ~Q
Premise

4 P & ~P
Join, 1, 2

Proof by contradiction:

5 ~~Q
Conclusion, 3

6 Q
Rem DNeg, 5

Conditional proof:

7 ~P => Q
Conclusion, 2

Conditional proof:

8 P => [~P => Q]
Conclusion, 1

And not a falsum in sight to confuse things!

[olcott]

It makes the principle of explosion impossible.

> Better is P & ~P => Q. It actually makes sense.
>

That seems psychotic to me.

> Better still is P => [~P => Q] (the principle of vacuous truth) which is quite useful in proofs.
>

The term {vacuous truth} makes as much sense as satisfying hunger with
non-existent food.

> Learn from my proofs here. This proof has 2 examples of discharging a premise using the Conclusion Rule on lines 4 and 6 .
>
> 1. P & ~P
> Premise
>
> 2. ~Q
> Premise
>
> 3. P & ~P
> Copy, 1
>
> Proof by contradiction:
>
> 4. ~~Q
> Conclusion, 2
>
> 5. Q
> Rem DNeg, 4
>
> Conditional proof:
>
> 6. P & ~P => Q
> Conclusion, 1
>

That is only true because of the stupid way that implication diverges
from if-then.

P Q if P then Q
0 0 ?
0 1 ?
1 0 0
1 1 0

> A variation discharging each premise using the Conclusion Rule on lines 5, 7 and 8:
>
> 1 P
> Premise
>
> 2 ~P
> Premise
>
> 3 ~Q
> Premise
>
> 4 P & ~P
> Join, 1, 2
>
> Proof by contradiction:
>
> 5 ~~Q
> Conclusion, 3
>
> 6 Q
> Rem DNeg, 5
>
> Conditional proof:
>
> 7 ~P => Q
> Conclusion, 2
>
> Conditional proof:
>
> 8 P => [~P => Q]
> Conclusion, 1
>
> And not a falsum in sight to confuse things!
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

[Dan Christensen]

On Tuesday, May 23, 2023 at 5:32:26 PM UTC-4, olcott wrote:

[snip]

> >>> Now look up how to discharge a premise/assumption to finish your proof. Then get back to us.
> >>>
> >> I already did discharge the premises when I converted P ∧ ¬P to False.
> >
> > Not very useful, I'm afraid.
> >
> It makes the principle of explosion impossible.

Wrong.

> > Better is P & ~P => Q. It actually makes sense.
> >

> That seems psychotic to me.

Only because it works and your "system" (whatever it may be) doesn't seem to. Cognitive dissonance? Talk to your shrink about it.

> > Better still is P => [~P => Q] (the principle of vacuous truth) which is quite useful in proofs.
> >

> The term {vacuous truth} makes as much sense as satisfying hunger with
> non-existent food.

On the contrary, I have found it to be very useful in actual proofs, especially in cases of empty sets (hence the "vacuous" bit).

> > Learn from my proofs here. This proof has 2 examples of discharging a premise using the Conclusion Rule on lines 4 and 6 .
> >
> > 1. P & ~P
> > Premise
> >
> > 2. ~Q
> > Premise
> >
> > 3. P & ~P
> > Copy, 1
> >
> > Proof by contradiction:
> >
> > 4. ~~Q
> > Conclusion, 2
> >
> > 5. Q
> > Rem DNeg, 4
> >
> > Conditional proof:
> >
> > 6. P & ~P => Q
> > Conclusion, 1
> >

> That is only true because of the stupid way that implication diverges
> from if-then.
>

[snip]

Wrong. See my recent posting here: https://math.stackexchange.com/questions/4703222/is-this-a-correct-interpretation-of-p-implies-q/4703291#4703291

[olcott]

Those are some extremely impressive stats.
What do you know about the Tarski Undefinability Theorem?

[Dan Christensen]

Thanks.

> What do you know about the Tarski Undefinability Theorem?

It is definitely outside my areas of interest. I'm more interested addressing logical and mathematical misperceptions common at the undergrad level, e.g. misperceptions about material implication, Peano's Axioms, and various supposed paradoxes.

[olcott]

Tarski's Undefinability Theorem derives its results entirely on the
basis of his formalization of the Liar Paradox. I have mostly focused on
pathological self-reference for the last 20 years.

Do you understand that Gödel's 1931 incompleteness theorem is isomorphic
to a paradox?

>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

I recently posted here a resolution of the Epimenides Paradox:

https://www.dcproof.com/EpimenidesParadox.htm

There was nothing "pathological" about it. Assuming his claim, "Cretans are always liars," is true leads to a contradiction, so it must be false and at least one Cretan once made a true statement.

> Do you understand that Gödel's 1931 incompleteness theorem is isomorphic
> to a paradox?

GIT is similarly outside of my areas of interest.

[olcott]

I never look at that version because it is not the simplest possible way
to do it. That version may be false.

What about: "This sentence is not true."
We can't say that it is true because this would make it false and we
can't say it is false because that would make it true.

Why has the Liar Paradox not had its self-reference error formalized before?
Every other investigation of the Liar Paradox conflated the testing of
its Boolean (truth) value and the derivation of this Boolean value as a
single atomic operation with no constituent parts. No one had previously
ever decomposed the atomic steps of a proposition’s Boolean (truth)
value transitioning from non-existence into existence. Only after a
proposition is formed can it be tested. Only after it has been tested
does it derive a Boolean (truth) value.

When we explicitly divide mathematical propositions into their two
semantic properties:
(1) Assertion // What it is claiming to be true
(2) Boolean.Value // The {True, False} value based on testing its Assertion

We can decompose every step of the translation of a Declarative Sentence
into its equivalent Mathematical Proposition. We no longer conflate the
testing of the assertion and the assignment of the Boolean result of
this testing as a single atomic step.

https://www.researchgate.net/publication/307442489_Formalizing_the_logical_self-reference_error_of_the_Liar_Paradox

>
>> Do you understand that Gödel's 1931 incompleteness theorem is isomorphic
>> to a paradox?
>
> GIT is similarly outside of my areas of interest.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

On Tuesday, May 23, 2023 at 9:15:58 PM UTC-4, olcott wrote:
[snip]

> >

> > I recently posted here a resolution of the Epimenides Paradox:
> >
> > https://www.dcproof.com/EpimenidesParadox.htm
> >
> > There was nothing "pathological" about it. Assuming his claim, "Cretans are always liars," is true leads to a contradiction, so it must be false and at least one Cretan once made a true statement.

> I never look at that version

It shows.

> because it is not the simplest possible way
> to do it. That version may be false.
>
> What about: "This sentence is not true."

That is NOT equivalent to a Cretan saying Cretans always lie. Again, assuming it is true leads to a contradiction, so it cannot be true, so it must be false. (See lines 6-16) Assuming it false leads to no contradiction. It leads only to at least one Cretan at least once making a true statement. (See lines 17-27)

"This sentence is not true" does not seem amenable to this kind analysis. Here, we have a statement S such that S => ~S is true. Here, as well, S must be false.

PROOF

1. S => ~S
Premise

2. S
Premise

3. ~S
Detach, 1, 2

4. S & ~S
Join, 2, 3

5. ~S
Conclusion, 2

6. [S => ~S] => ~S
Conclusion, 1

[olcott]

On 5/23/2023 10:19 PM, Dan Christensen wrote:
> On Tuesday, May 23, 2023 at 9:15:58 PM UTC-4, olcott wrote:
> [snip]
>
>>>
>>> I recently posted here a resolution of the Epimenides Paradox:
>>>
>>> https://www.dcproof.com/EpimenidesParadox.htm
>>>
>>> There was nothing "pathological" about it. Assuming his claim, "Cretans are always liars," is true leads to a contradiction, so it must be false and at least one Cretan once made a true statement.
>
>> I never look at that version
>
> It shows.
>
>> because it is not the simplest possible way
>> to do it. That version may be false.
>>
>> What about: "This sentence is not true."
>
> That is NOT equivalent to a Cretan saying Cretans always lie. Again, assuming it is true leads to a contradiction, so it cannot be true, so it must be false.

If it is false then the assertion that it is untrue becomes true thus
another contradiction. I have owned LiarParadox.org as the website
where I originally published my work. I have spent thousands of hours
on it. It is simply not a truth bearer, the same way that
What time is it? is not a truth bearer.

> (See lines 6-16) Assuming it false leads to no contradiction. It leads only to at least one Cretan at least once making a true statement. (See lines 17-27)
>
> "This sentence is not true" does not seem amenable to this kind analysis. Here, we have a statement S such that S => ~S is true. Here, as well, S must be false.
>
> PROOF
>
> 1. S => ~S
> Premise
>
> 2. S
> Premise
>
> 3. ~S
> Detach, 1, 2
>
> 4. S & ~S
> Join, 2, 3
>
> 5. ~S
> Conclusion, 2
>
> 6. [S => ~S] => ~S
> 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
>

[Ross Finlayson]

So, you're shilling a brief freshman course for non-majors with simply excluding that which isn't in it?

And proving that "material" implication is fallacious reasoning?

Or, seems you left that part out, ....

[Dan Christensen]

On Tuesday, May 23, 2023 at 11:53:02 PM UTC-4, olcott wrote:
> On 5/23/2023 10:19 PM, Dan Christensen wrote:
> > On Tuesday, May 23, 2023 at 9:15:58 PM UTC-4, olcott wrote:
> > [snip]
> >
> >>>
> >>> I recently posted here a resolution of the Epimenides Paradox:
> >>>
> >>> https://www.dcproof.com/EpimenidesParadox.htm
> >>>
> >>> There was nothing "pathological" about it. Assuming his claim, "Cretans are always liars," is true leads to a contradiction, so it must be false and at least one Cretan once made a true statement.
> >
> >> I never look at that version
> >
> > It shows.
> >
> >> because it is not the simplest possible way
> >> to do it. That version may be false.
> >>
> >> What about: "This sentence is not true."
> >
> > That is NOT equivalent to a Cretan saying Cretans always lie. Again, assuming it is true leads to a contradiction, so it cannot be true, so it must be false.

> If it is false then the assertion that it is untrue becomes true thus
> another contradiction.

No, it infers that at least one Cretan at least once made a true statement.

> I have owned LiarParadox.org as the website
> where I originally published my work. I have spent thousands of hours
> on it.

It's good to have a hobby. Maybe you can post my proof: https://www.dcproof.com/EpimenidesParadox.htm

> It is simply not a truth bearer, the same way that
> What time is it? is not a truth bearer.

Ummm... What are its advantages of your proposed system, Pete? Can you now solve more problems? Or maybe FEWER problems?

> > (See lines 6-16) Assuming it false leads to no contradiction. It leads only to at least one Cretan at least once making a true statement. (See lines 17-27)
> >

> > "This sentence is not true" does not seem amenable to this kind analysis. Here, we have a statement S such that [the implication] S => ~S is true. Here, as well, S must be false.

[olcott]

On 5/23/2023 11:24 PM, Dan Christensen wrote:
> On Tuesday, May 23, 2023 at 11:53:02 PM UTC-4, olcott wrote:
>> On 5/23/2023 10:19 PM, Dan Christensen wrote:
>>> On Tuesday, May 23, 2023 at 9:15:58 PM UTC-4, olcott wrote:
>>> [snip]
>>>
>>>>>
>>>>> I recently posted here a resolution of the Epimenides Paradox:
>>>>>
>>>>> https://www.dcproof.com/EpimenidesParadox.htm
>>>>>
>>>>> There was nothing "pathological" about it. Assuming his claim, "Cretans are always liars," is true leads to a contradiction, so it must be false and at least one Cretan once made a true statement.
>>>
>>>> I never look at that version
>>>
>>> It shows.
>>>
>>>> because it is not the simplest possible way
>>>> to do it. That version may be false.
>>>>
>>>> What about: "This sentence is not true."
>>>
>>> That is NOT equivalent to a Cretan saying Cretans always lie. Again, assuming it is true leads to a contradiction, so it cannot be true, so it must be false.
>
>> If it is false then the assertion that it is untrue becomes true thus
>> another contradiction.
>
> No, it infers that at least one Cretan at least once made a true statement.
>
>> I have owned LiarParadox.org as the website
>> where I originally published my work. I have spent thousands of hours
>> on it.
>
> It's good to have a hobby. Maybe you can post my proof: https://www.dcproof.com/EpimenidesParadox.htm
>
>> It is simply not a truth bearer, the same way that
>> What time is it? is not a truth bearer.
>
> Ummm... What are its advantages of your proposed system, Pete? Can you now solve more problems? Or maybe FEWER problems?

My goal is to have a chat bot that can take on each individual on social
media and very effectively quell any disinformation by arguing against
it so effectively that the disinformation is cut off before it can
start.

[Dan Christensen]

DC Proof is intended as a brief introductory course (2nd year?) introducing math majors to the basic methods of proof to prepare them for more proof-oriented, less procedural courses like real analysis.

> And proving that "material" implication is fallacious reasoning?
>

Sorry, but nonsense like that could be a real career ender for math majors. Is that what happened to you, Ross? Couldn't get past P => Q?

[Ross Finlayson]

Sounds like seventh grade , ....

[Ross Finlayson]

(I got everything I need from _direct_ implication, and
false antecedents don't have any connective of the conditional,
except the bi-conditional where false <-> false. In the language
here there are constants for "true" and "false", distinct.)

I have a math degree and some work experience...,
I got my fingerprints so after a brief practicum could
be in front of a public classroom.

As above, establishing "Not LEM" means disambiguation is to follow,
here that being the rejection of logical fallacies, like establishing
"material implication does not reflect a temporal modality",
to reject the fallacy "implication isn't implication when the antecedent's false,
and it is, too, Not LEM". The "material" implication violates LEM.

[olcott]

People on SE Math rank him in the top 3%

[olcott]

I totally agree with you on this.
Where classical logic diverges from relevance logic classical logic
diverges from correct reasoning.
https://plato.stanford.edu/entries/logic-relevance/

> I have a math degree and some work experience...,
> I got my fingerprints so after a brief practicum could
> be in front of a public classroom.
>
> As above, establishing "Not LEM" means disambiguation is to follow,
> here that being the rejection of logical fallacies, like establishing
> "material implication does not reflect a temporal modality",
> to reject the fallacy "implication isn't implication when the antecedent's false,
> and it is, too, Not LEM". The "material" implication violates LEM.
>
>

[Dan Christensen]

On Wednesday, May 24, 2023 at 11:54:26 AM UTC-4, olcott wrote:
> On 5/24/2023 10:46 AM, Ross Finlayson wrote:

[snip]

> I totally agree with you on this.
> Where classical logic diverges from relevance logic classical logic
> diverges from correct reasoning.

You might get somewhere with your new system of logic if you could somehow show that classical logic is somehow inconsistent and leads to errors in applications even when properly applied. Until then...

[olcott]

On 5/24/2023 11:55 AM, Dan Christensen wrote:
> On Wednesday, May 24, 2023 at 11:54:26 AM UTC-4, olcott wrote:
>> On 5/24/2023 10:46 AM, Ross Finlayson wrote:
> [snip]
>
>> I totally agree with you on this.
>> Where classical logic diverges from relevance logic classical logic
>> diverges from correct reasoning.
>
> You might get somewhere with your new system of logic if you could somehow show that classical logic is somehow inconsistent and leads to errors in applications even when properly applied. Until then...

I just realized that the Principle of Explosion is understood to diverge
from correct reasoning in that it is commonly understood to simply
ignore the law of non contradiction.


The problem in this case is that the key errors that are made in
classical logic are things that you have no interest in:
Gödel 1931 Incompleteness and Tarski undefinability.
False ⇒ {any damn thing you want} is not truth preserving.

All of the divergence of classical logic from correct reasoning is
easily corrected establishing the foundation of analytical truth.

Analytical truth includes all of math and all of logic and every other
expression of formal or natural language that can be verified as totally
true entirely on the basis of its semantic meaning.

*When analytically true means*
(a) Finite strings are stipulated to have the semantic property of
Boolean true.

Only by stipulating relations between finite strings do finite strings
acquire semantic meaning otherwise they remain utterly meaningless. All
of these stipulated relations are stipulated to have the semantic
property of Boolean true. This makes these finite strings tautologies
that we know must be true.

(b) Finite strings are semantically deduced from the above set.
(sound deductive inference)

Undefinability and incompleteness and all other divergence from correct
reasoning cannot occur. (a) simply defines the meaning of terms in the
correct model of the world.

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

On Wednesday, May 24, 2023 at 1:53:54 PM UTC-4, olcott wrote:
> On 5/24/2023 11:55 AM, Dan Christensen wrote:
> > On Wednesday, May 24, 2023 at 11:54:26 AM UTC-4, olcott wrote:
> >> On 5/24/2023 10:46 AM, Ross Finlayson wrote:
> > [snip]
> >
> >> I totally agree with you on this.
> >> Where classical logic diverges from relevance logic classical logic
> >> diverges from correct reasoning.
> >
> > You might get somewhere with your new system of logic if you could somehow show that classical logic is somehow inconsistent and leads to errors in applications even when properly applied. Until then...
> I just realized that the Principle of Explosion is understood to diverge
> from correct reasoning in that it is commonly understood to simply
> ignore the law of non contradiction.
>
>
> The problem in this case is that the key errors that are made in
> classical logic are things that you have no interest in:
> Gödel 1931 Incompleteness and Tarski undefinability.
> False ⇒ {any damn thing you want} is not truth preserving.
>

How is A & ~A => B not "truth preserving?" It is a tautology.

[olcott]

I am actually referring to the truth table of ⇒
that has True entailed by False on lines 3 and 4

p---q---p ⇒ q
T---T---T
T---F---F
F---T---T
F---F---T

I am not sure if this is an actual non-truth preserving issue,
yet it is obvious that ⇒ is not the conventional way that the
semantics of if-then actually works.

p---q---if p then q
T---T---T
T---F---F
F---T---? unknown
F---F---? unknown

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

[Dan Christensen]

On Wednesday, May 24, 2023 at 2:41:15 PM UTC-4, olcott wrote:
> On 5/24/2023 1:21 PM, Dan Christensen wrote:

> >> The problem in this case is that the key errors that are made in
> >> classical logic are things that you have no interest in:
> >> Gödel 1931 Incompleteness and Tarski undefinability.
> >> False ⇒ {any damn thing you want} is not truth preserving.
> >>
> >
> > How is A & ~A => B not "truth preserving?" It is a tautology.
> >
> I am actually referring to the truth table of ⇒
> that has True entailed by False on lines 3 and 4
>

How is that a problem? These are features of material implication that are admittedly rarely if ever used in daily discourse, but they are useful in very technical arguments (e.g .mathematical proofs). These features are easy to justify from what might be called first principles:

Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)

Suppose A is false

1. ~A
Premise

Suppose A is true

2. A
Premise

Suppose B is false

3. ~B
Premise

4. ~A & A
Join, 1, 2

5. ~~B
Conclusion, 3

6. B
Rem DNeg, 5

7. A => B
Conclusion, 2

8. ~A => [A => B]
Conclusion, 1

Which line if any here do you imagine is invalid and why?

> p---q---p ⇒ q
> T---T---T
> T---F---F
> F---T---T
> F---F---T
>
> I am not sure if this is an actual non-truth preserving issue,
> yet it is obvious that ⇒ is not the conventional way that the
> semantics of if-then actually works.
>
> p---q---if p then q
> T---T---T
> T---F---F
> F---T---? unknown
> F---F---? unknown

Not necessary. There is no logical justification for it.

[olcott]

On 5/24/2023 2:15 PM, Dan Christensen wrote:
> On Wednesday, May 24, 2023 at 2:41:15 PM UTC-4, olcott wrote:
>> On 5/24/2023 1:21 PM, Dan Christensen wrote:
>
>>>> The problem in this case is that the key errors that are made in
>>>> classical logic are things that you have no interest in:
>>>> Gödel 1931 Incompleteness and Tarski undefinability.
>>>> False ⇒ {any damn thing you want} is not truth preserving.
>>>>
>>>
>>> How is A & ~A => B not "truth preserving?" It is a tautology.
>>>
>> I am actually referring to the truth table of ⇒
>> that has True entailed by False on lines 3 and 4
>>
>
> How is that a problem? These are features of material implication that are admittedly rarely if ever used in daily discourse, but they are useful in very technical arguments (e.g .mathematical proofs). These features are easy to justify from what might be called first principles:
>
> Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)
>
> Suppose A is false
>
> 1. ~A
> Premise
>
> Suppose A is true
>
> 2. A
> Premise
>

These premises cancel each other out thus must be removed or logic
diverges from correct reasoning. This cuts off the rest of the proof.

>> p---q---if p then q
>> T---T---T
>> T---F---F
>> F---T---? unknown
>> F---F---? unknown
>
> Not necessary. There is no logical justification for it.

Yes semantically if you know that p entails q and you know that p is
false then you have no idea what the truth value of q is.

>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

[Dan Christensen]

On Wednesday, May 24, 2023 at 4:13:39 PM UTC-4, olcott wrote:
> On 5/24/2023 2:15 PM, Dan Christensen wrote:
> > On Wednesday, May 24, 2023 at 2:41:15 PM UTC-4, olcott wrote:
> >> On 5/24/2023 1:21 PM, Dan Christensen wrote:
> >
> >>>> The problem in this case is that the key errors that are made in
> >>>> classical logic are things that you have no interest in:
> >>>> Gödel 1931 Incompleteness and Tarski undefinability.
> >>>> False ⇒ {any damn thing you want} is not truth preserving.
> >>>>
> >>>
> >>> How is A & ~A => B not "truth preserving?" It is a tautology.
> >>>
> >> I am actually referring to the truth table of ⇒
> >> that has True entailed by False on lines 3 and 4
> >>
> >
> > How is that a problem? These are features of material implication that are admittedly rarely if ever used in daily discourse, but they are useful in very technical arguments (e.g .mathematical proofs). These features are easy to justify from what might be called first principles:
> >
> > Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)
> >
> > Suppose A is false
> >
> > 1. ~A
> > Premise
> >
> > Suppose A is true
> >
> > 2. A
> > Premise
> >
> These premises cancel each other out thus must be removed or logic
> diverges from correct reasoning. This cuts off the rest of the proof.

How does one premise "cancel out" another? Note that there is no requirement that one premise be consistent with another. Your system of logic should be able to handle it. (See "proof by contradiction.")

> >> p---q---if p then q
> >> T---T---T
> >> T---F---F
> >> F---T---? unknown
> >> F---F---? unknown
> >
> > Not necessary. There is no logical justification for it.

> Yes semantically if you know that p entails q and you know that p is
> false then you have no idea what the truth value of q is.

Agreed, but so what? As I have proven, if the antecedent is false, the implication will be true regardless of the truth value of consequent. It follows trivially from what might be called "first principles."

That proof again:

Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)

Suppose A is false

1. ~A
Premise

Suppose A is true

2. A
Premise

Suppose B is false

3. ~B
Premise

4. ~A & A
Join, 1, 2

5. ~~B
Conclusion, 3

6. B
Rem DNeg, 5

7. A => B
Conclusion, 2

8. ~A => [A => B]
Conclusion, 1

[olcott]

On 5/24/2023 3:34 PM, Dan Christensen wrote:
> On Wednesday, May 24, 2023 at 4:13:39 PM UTC-4, olcott wrote:
>> On 5/24/2023 2:15 PM, Dan Christensen wrote:
>>> On Wednesday, May 24, 2023 at 2:41:15 PM UTC-4, olcott wrote:
>>>> On 5/24/2023 1:21 PM, Dan Christensen wrote:
>>>
>>>>>> The problem in this case is that the key errors that are made in
>>>>>> classical logic are things that you have no interest in:
>>>>>> Gödel 1931 Incompleteness and Tarski undefinability.
>>>>>> False ⇒ {any damn thing you want} is not truth preserving.
>>>>>>
>>>>>
>>>>> How is A & ~A => B not "truth preserving?" It is a tautology.
>>>>>
>>>> I am actually referring to the truth table of ⇒
>>>> that has True entailed by False on lines 3 and 4
>>>>
>>>
>>> How is that a problem? These are features of material implication that are admittedly rarely if ever used in daily discourse, but they are useful in very technical arguments (e.g .mathematical proofs). These features are easy to justify from what might be called first principles:
>>>
>>> Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)
>>>
>>> Suppose A is false
>>>
>>> 1. ~A
>>> Premise
>>>
>>> Suppose A is true
>>>
>>> 2. A
>>> Premise
>>>
>> These premises cancel each other out thus must be removed or logic
>> diverges from correct reasoning. This cuts off the rest of the proof.
>
> How does one premise "cancel out" another? Note that there is no requirement that one premise be consistent with another. Your system of logic should be able to handle it. (See "proof by contradiction.")

When anyone makes contradictory statements we know that they are lying
so we dismiss what they say on this basis. When logic does not do the
same it diverges fro correct reasoning.

>>>> p---q---if p then q
>>>> T---T---T
>>>> T---F---F
>>>> F---T---? unknown
>>>> F---F---? unknown
>>>
>>> Not necessary. There is no logical justification for it.
>
>> Yes semantically if you know that p entails q and you know that p is
>> false then you have no idea what the truth value of q is.
>
> Agreed, but so what? As I have proven, if the antecedent is false, the implication will be true regardless of the truth value of consequent.

That does not seem to be truth preserving.

> It follows trivially from what might be called "first principles."
>
> That proof again:
>
> Prove: ~A => [A => B] (covers both lines 3 and 4 of the truth table where A is false.)
>
> Suppose A is false
>
> 1. ~A
> Premise
>
> Suppose A is true
>
> 2. A
> Premise
>

These two premises have proved to be liars so failing to ignore them
diverges from correct reasoning.

[Dan Christensen]

[snip]

It seems your proposed system of logic cannot handle contradictions. It's easy in ordinary logic.

The Simplest Example : A Proof by Contradiction

1. A & ~A
Premise

2 ~[A & ~A]
Conclusion, 1

In other words, A & ~A is always false.

[olcott]

The way that correct reasoning actually works is that contradictions
prove untruth. For years I thought that the Principle of Explosion was
considered valid logic and not merely a hypothetical what-if we ignore
the law of non contradiction?

My system handles contradictory premises properly by removing them.

[Ross Finlayson]

Hm.

Is "X => Y" valid?

Here "X" is "you know the value of X".

How about X => X?

So, if you don't know X, then, you think X => Y is valid,
but, you don't even know what it is.

And, if you do, it's not. (It would just be a stipulation, and, you know, unfounded.)

And, if you don't know X, then you get ~X => X, and X => X. contradicting yourself.

Either way what you got there is "A -> A", at best.



Material implication is fraught with ambiguity, and,
about proofs by contradiction, they don't really much
prove things true, just what things are not true,
then that in a wider world are what things are true.


Then, proofs by contradiction are of course a very basic reflection on
the scientific method and falsifiability and the statistical method and
invalidation of the hypothesis.

So, your unscientific approach to incomplete logics is rejected, by many.


So, it seems best you do is show via proof-by-contradiction that the
contradictory premises can not both be true.


Again, about the direct implication, there's X -> X, it's tautological,
and ~X -> ~X, it's tautological.

But, about material implication, there's ~X => ~X, whether X is false,
it would contradict itself, or X is true, contradict itself.

You don't have truth-values in your little setup.


Of course, modern foundations is often framed in a constructivist sense
in the usual sense that proofs-via-contradiction are un-used, though, of
course, proofs via causality and the contrapositive are perfectly valid,
in Boolean expressions, and extended truth-tables.

[Dan Christensen]

> The way that correct reasoning actually works is that contradictions
> prove untruth.

If you derive a contradiction from an assumption , correct reasoning tells you that your assumption that is false.

> For years I thought that the Principle of Explosion was
> considered valid logic and not merely a hypothetical what-if we ignore
> the law of non contradiction?

As I have shown here from first principles, ~P => [P => Q] is true for any propositions P and Q.

> My system handles contradictory premises properly by removing them.

Good luck deriving very much in math on that basis. But maybe that's not a consideration for you?

[olcott]

Thus A, ~A as premises must be converted to False nullifying them
instead of using one of these premises in a proof and ignoring the
other. This this proof is incorrect:

*Step --- Proposition --- Derivation*
1 -------- P ------------ Assumption
2 ------- ¬P ------------ Assumption
3 -------- P ∨ Q -------- Disjunction introduction (1)
4 -------- Q ------------ Disjunctive syllogism (3,2)

>> For years I thought that the Principle of Explosion was
>> considered valid logic and not merely a hypothetical what-if we ignore
>> the law of non contradiction?
>
> As I have shown here from first principles, ~P => [P => Q] is true for any propositions P and Q.

Only because => is a screwy divergence from if-then.

>> My system handles contradictory premises properly by removing them.
>
> Good luck deriving very much in math on that basis. But maybe that's not a consideration for you?

If math derives anything besides {false} from contradictory premises
then math diverges from truth.

Try and show any example where simply canceling out contradictory
premises makes math unable to express important relationships.

>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

On Thursday, May 25, 2023 at 2:35:32 PM UTC-4, Ross Finlayson wrote:

>
> Is "X => Y" valid?
>

It is true when it is not case that both X is true and Y is false.

> Here "X" is "you know the value of X".
>
> How about X => X?
>

Always true.

> So, if you don't know X, then, you think X => Y is valid,
> but, you don't even know what it is.
>
> And, if you do, it's not. (It would just be a stipulation, and, you know, unfounded.)
>
> And, if you don't know X, then you get ~X => X, and X => X. contradicting yourself.
>

[snip]

X => X is true regardless of the truth value of X (whether true or false).

>
>
> Material implication is fraught with ambiguity,

It could not be more precise.

> and,
> about proofs by contradiction, they don't really much
> prove things true, just what things are not true,
> then that in a wider world are what things are true.
>

Is that supposed to be an excuse for not doing your math proofs?

>
> Then, proofs by contradiction are of course a very basic reflection on
> the scientific method and falsifiability and the statistical method and
> invalidation of the hypothesis.
>

What errors (not just counter-intuitive results) do you see arising in science from proofs by contradiction. Can you give an example?

> So, your unscientific approach to incomplete logics is rejected, by many.
>

The vast majority of mathematicians accept the validity proofs by contradiction. Must be frustrating as hell for you.

>
> So, it seems best you do is show via proof-by-contradiction that the
> contradictory premises can not both be true.
>

(~P => Q & ~Q) => P is a widely accepted tautology. Likewise (~P => (Q <=> ~Q)) => P. Deal with it.

>
> Again, about the direct implication, there's X -> X, it's tautological,
> and ~X -> ~X, it's tautological.

Yes. We have:

1. X
Premise

2. X => X
Conclusion, 1

AND...

1. ~X
Premise

2. ~X => ~X
Conclusion, 1

>
> But, about material implication, there's ~X => ~X, whether X is false,
> it would contradict itself, or X is true, contradict itself.
>

[snip]

Wrong.

Case 1: X is true

1. X
Premise

2. ~X
Premise

3. ~X => ~X
Conclusion, 2

4. X => [~X => ~X]
Conclusion, 1

Case 2: X is false

1. ~X
Premise

2. ~X
Premise

3. ~X => ~X
Conclusion, 2

4. ~X => [~X => ~X]
Conclusion, 1

In every case, we have ~X => ~X

[Dan Christensen]

[snip]

Wrong. There is no need to "convert" anything here.

> instead of using one of these premises in a proof and ignoring the
> other. This this proof is incorrect:
>
> *Step --- Proposition --- Derivation*
> 1 -------- P ------------ Assumption
> 2 ------- ¬P ------------ Assumption
> 3 -------- P ∨ Q -------- Disjunction introduction (1)
> 4 -------- Q ------------ Disjunctive syllogism (3,2)

Again, you have not completed this "proof". You need 2 more statements:

5 -------- ~P => Q -------------- Discharge 2, 4
6 -------- P => (~P => Q) ---- Discharge 1, 5

[olcott]

In other words you are saying that although ending up with a
contradiction proves that the argument is unsound that we can start a
sound argument with a contradiction?

>> instead of using one of these premises in a proof and ignoring the
>> other. This this proof is incorrect:
>>
>> *Step --- Proposition --- Derivation*
>> 1 -------- P ------------ Assumption
>> 2 ------- ¬P ------------ Assumption
>> 3 -------- P ∨ Q -------- Disjunction introduction (1)
>> 4 -------- Q ------------ Disjunctive syllogism (3,2)
>
> Again, you have not completed this "proof". You need 2 more statements:
>

If you think it is wrong then go edit the Wikipedia page it is a direct
quote: https://en.wikipedia.org/wiki/Principle_of_explosion#Proof

> 5 -------- ~P => Q -------------- Discharge 2, 4
> 6 -------- P => (~P => Q) ---- Discharge 1, 5
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>

[Ross Finlayson]

Not constructivists - in fact it's exactly what they reject.

(... Or, at least some of them. https://plato.stanford.edu/entries/mathematics-constructive/ )



Nope, X is a variable.


In your step 3 there, you have ~X, so, X => ~X.

"Applying material implications false antecedent materially implying anything."

In fact, anywhere you set up your case for contradiction,
you've proven material implication arrives at the opposite of what you, ..., "want".

Though, you ignore it, which is considered unconvincing.

[Dan Christensen]

Ending up with a contradiction proves only that the corresponding assumption/premise is false. In that case, I don't know that the notion of soundness is meaningful.

> >> instead of using one of these premises in a proof and ignoring the
> >> other. This this proof is incorrect:
> >>
> >> *Step --- Proposition --- Derivation*
> >> 1 -------- P ------------ Assumption
> >> 2 ------- ¬P ------------ Assumption
> >> 3 -------- P ∨ Q -------- Disjunction introduction (1)
> >> 4 -------- Q ------------ Disjunctive syllogism (3,2)
> >
> > Again, you have not completed this "proof". You need 2 more statements:
> >

> If you think it is wrong then go edit the Wikipedia page it is a direct
> quote: https://en.wikipedia.org/wiki/Principle_of_explosion#Proof

> > 5 -------- ~P => Q -------------- Discharge 2, 4
> > 6 -------- P => (~P => Q) ---- Discharge 1, 5
> >

Do you not understand what it means to discharge a premise?

[Dan Christensen]

On Thursday, May 25, 2023 at 11:04:07 PM UTC-4, Ross Finlayson wrote:
> On Thursday, May 25, 2023 at 3:29:32 PM UTC-7, Dan Christensen wrote:

[snip]

> > > But, about material implication, there's ~X => ~X, whether X is false,
> > > it would contradict itself, or X is true, contradict itself.
> > >
> > [snip]
> >
> > Wrong.
> >
> > Case 1: X is true
> >
> > 1. X
> > Premise
> >
> > 2. ~X
> > Premise
> >
> > 3. ~X => ~X
> > Conclusion, 2
> >
> > 4. X => [~X => ~X]
> > Conclusion, 1
> >
> > Case 2: X is false
> >
> > 1. ~X
> > Premise
> >
> > 2. ~X
> > Premise
> >
> > 3. ~X => ~X
> > Conclusion, 2
> >
> > 4. ~X => [~X => ~X]
> > Conclusion, 1
> >
> > In every case, we have ~X => ~X

> Not constructivists - in fact it's exactly what they reject.
>

Recall that I said, "The VAST MAJORITY of mathematicians accept the validity proofs by contradiction." Do you not agree?

> (... Or, at least some of them. https://plato.stanford.edu/entries/mathematics-constructive/ )
>
>
>
> Nope, X is a variable.
>

Here, it is logical proposition.

>
> In your step 3 there, you have ~X, so, X => ~X.
>

I think you mean ~X => ~X. Nothing wrong with that.

Again, we have Case 1: X is true

1. X
Premise

2. ~X
Premise

3. ~X => ~X <----------------------------- Here

Conclusion, 2

4. X => [~X => ~X]
Conclusion, 1

> "Applying material implications false antecedent materially implying anything."
>

[snip]

Misleading. Again, we have: ~P => [P => Q] for any proposition Q. From this, we cannot infer that Q is true. Or that Q is false.

[olcott]

Discharge means to get rid of. He was discharged from the Army.

In the natural deduction calculus, an assumption is discharged when the
conclusion of an inference does not depend on it, although one of the
premises of the inference does.
https://users.cecs.anu.edu.au/~jks/LogicNotes/glossary/g_discharge.html

Unless we ignore the law of non-contradiction we must have P, ¬P
translated into false before we begin the above proof.

This elimination rule agrees.
(¬E) φ, ¬φ ⊢ ⊥
https://iep.utm.edu/natural-deduction/#H4
When we do that we can no longer use Disjunction introduction because it
is not truth preserving.

> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

[Dan Christensen]

Not very useful definitions. No wonder you are confused.

In the above proof, the conclusion on line 5 is derived from line 2 (the corresponding premise) and line 4 (the previous statement), inserting '=>' between them. Lines 2-4 will not then be accessible on subsequent lines of the proof having been essentially "deactivated." If the previous statement had been a contradiction of the form P & ~P, the conclusion would simply be the negation of the corresponding premise.

Similarly, the conclusion on line 6 is derived from line 1 (the corresponding premise) and line 5 (the previous statement).

I hope this helps.

[olcott]

It seems that you are great at presenting the "received view" yet like
all mathematicians and logicians totally unable to avoid rejecting
philosophy of logic and math out-of-hand without review.

Mathematicians and logicians treat this "received view" as if is
necessarily infallible. From a religious point of view this would be
blasphemy. No sense digressing here though.

It is a divergence from correct reasoning when someone points out
inconsistencies in this "received view" and they are simply ignored
because this "received view" is construed as infallible.

Unless the law of non-contradiction is explicitly ignored a pair of
contradictory premises must be translated into False before correct
inference can possibly proceed. This means that the above proof
steps of 1-4 are dead in the water after steps 1 and 2 are translated
into False.

That you believe otherwise simply because that is not the way that it is
conventionally done is an error of reasoning.

[Richard Damon]

Anythinng that HAS contradictory premise diverges from truth.

>
> Try and show any example where simply canceling out contradictory
> premises makes math unable to express important relationships.

So, you just don't understand how logic works. Apply the rule to your
own logic, and your system just disappears.

[olcott]

I agree with you, yet the quoted proof of the Principle of explosion
provided above disagrees.

Once proof steps(1,2) P, ¬P are translated into False by this rule of
natural deduction (¬E) φ, ¬φ ⊢ ⊥
https://iep.utm.edu/natural-deduction/#H4
step 3 cannot occur.

>
>>
>> Try and show any example where simply canceling out contradictory
>> premises makes math unable to express important relationships.
>
> So, you just don't understand how logic works. Apply the rule to your
> own logic, and your system just disappears.
>
>>
>>>
>>> Dan
>>>
>>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>>> Visit my Math Blog at http://www.dcproof.wordpress.com
>>
>

[Richard Damon]

I thought you finally understood the principle of explosion in the othr
forum.

The principle of explosion says that once a system admits into it a
contradiction, then the system totally breaks as you can prove anything.

Yes, if you hypothesize a contradiction, you have hypothesized an
explosion, but that just says a hypothetical explosion until you find a
case where the hypothesis is actually true.

Once a systen has been found to be able to prove from its fundamental
truth-makers that both P, and ~P are provably true, the system is found
to be actually exploded. The root of the problm isn't in showing that P
and ~P are both true, but goes deeper that the set of truth-makers for
that system must be inconsistent, and from that inconsistency, all sorts
of errors can be proven.

It seems you can't remember what you learned just a few days ago, I
guess your mind is really that shot.

[Dan Christensen]

[snip]

What did you expect? Classical logic has proven so valuable in so many applications for centuries, perhaps millennia. If some philosopher now wants to make a name for himself by demanding that it be replaced by something radically different, it's going to be a very hard sell indeed.

Dan

[olcott]

I am only expecting logicians to be able to comprehend that there are
inconsistencies between the use of contradictions at the beginning of a
proof and deriving a contradiction at the end of a proof.

At the end of a proof a contradiction indicates that one or more of the
assumptions are false. To be consistent it must be treated this same way
at the beginning of the proof.

It seems that logicians are like religious people the inconsistencies in
logic are treated just like the inconsistencies in the bible as
infallible words. Ludwig Wittgenstein had this same issue with logicians
and mathematicians.

[Richard Damon]

So, you don't understand what the principle of explosion is trying to show.

Without the principle of explosion, we might be tempted to say it was ok
if a system happened to be able to, in some corner cases, prove a
contradiciton in some minor areas. It is BECAUSE of the principle of
explosion that we know we must reject any system that it is shown to be
able to prove a contradiction, no matter how minor.

Again, the principle of explosion, by its own admission, says NOTHING
about systems that can not prove a contradictory set of statements,
because they do not meet its requirements. What it shows is that we MUST
totally reject any system that can prove such a pair of statments, no
matter how minor the contradiction seems to be.

The sole exception, is for systems that so restrict the power of logic
in them that the proof of the principle of explosion can not be done in
them, like system that say premises to a logical operation need to be
simple atomics (so we can't use the fact that "P|Q" is true as a premise
to an arguement), such system do not explode, but also end up very
restricted and limited.

[Dan Christensen]

On Friday, May 26, 2023 at 1:48:16 PM UTC-4, olcott wrote:
> On 5/26/2023 12:25 PM, Dan Christensen wrote:

[snip]

> >> It seems that you are great at presenting the "received view" yet like
> >> all mathematicians and logicians totally unable to avoid rejecting
> >> philosophy of logic and math out-of-hand without review.
> >>
> >> Mathematicians and logicians treat this "received view" as if is
> >> necessarily infallible.
> >
> > [snip]
> >
> > What did you expect? Classical logic has proven so valuable in so many applications for centuries, perhaps millennia. If some philosopher now wants to make a name for himself by demanding that it be replaced by something radically different, it's going to be a very hard sell indeed.
> >

> I am only expecting logicians to be able to comprehend that there are
> inconsistencies between the use of contradictions at the beginning of a
> proof and deriving a contradiction at the end of a proof.
>

It is not enough to simply make such claims. You have to prove them using accepted methods of proof.

THEOREM: A & ~A is false

PROOF:

1. A & ~A
Premise

2. ~[A & ~A]
Conclusion, 1

[Ross Finlayson]

Nope, just get rid of material implication
by putting in "ex falso nihilum", and keep
all the great things otherwise about the tableau
and the calculi.

Then, just framing that "as far as your non-logical objects go,
contradiction is suitable for the scientific and statistical methods,
if you'd bother to know their philosophies what's acceptable about
falsification and invalidation of the hypothesis".

Then one might say that the classical is just sort of a weak sort of science,
in its non-constructivist results, while still that all constructivist results hold
as classically.

I.e., don't be fooled: constructivists perfectly adhere to positive inference.

[Ross Finlayson]

(... or incomplete.)

[olcott]

Yes that is what I have been saying.
Or we could say the same thing this way: ⊥ ⊢ ⊥

> Then, just framing that "as far as your non-logical objects go,
> contradiction is suitable for the scientific and statistical methods,
> if you'd bother to know their philosophies what's acceptable about
> falsification and invalidation of the hypothesis".
>
> Then one might say that the classical is just sort of a weak sort of science,
> in its non-constructivist results, while still that all constructivist results hold
> as classically.
>
> I.e., don't be fooled: constructivists perfectly adhere to positive inference.
>
>

[olcott]

On 5/26/2023 1:17 PM, Dan Christensen wrote:
> On Friday, May 26, 2023 at 1:48:16 PM UTC-4, olcott wrote:
>> On 5/26/2023 12:25 PM, Dan Christensen wrote:
> [snip]
>
>>>> It seems that you are great at presenting the "received view" yet like
>>>> all mathematicians and logicians totally unable to avoid rejecting
>>>> philosophy of logic and math out-of-hand without review.
>>>>
>>>> Mathematicians and logicians treat this "received view" as if is
>>>> necessarily infallible.
>>>
>>> [snip]
>>>
>>> What did you expect? Classical logic has proven so valuable in so many applications for centuries, perhaps millennia. If some philosopher now wants to make a name for himself by demanding that it be replaced by something radically different, it's going to be a very hard sell indeed.
>>>
>
>> I am only expecting logicians to be able to comprehend that there are
>> inconsistencies between the use of contradictions at the beginning of a
>> proof and deriving a contradiction at the end of a proof.
>>
>
> It is not enough to simply make such claims. You have to prove them using accepted methods of proof.
>

These two are already axioms:

(¬E) φ, ¬φ ⊢ ⊥
https://iep.utm.edu/natural-deduction/#H4

Then ⊥ ⊢ ⊥ // same as P ⊢ P
eliminates explosion.

> THEOREM: A & ~A is false
>
> PROOF:
>
> 1. A & ~A
> Premise
>
> 2. ~[A & ~A]
> 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
>

[Jeff Barnett]

If, rather than a philosopher, a fool made the suggestion it would be
even harder to sell. Wat do you think?
--
Jeff Barnett

[Dan Christensen]

My guess is their chances would be about equal.

Dan

[olcott]

If we do not overturn the Tarski Undefinability theorem such that true
can be computationally divided from untrue humanity may perish.

Severe anthropogenic climate change proven entirely with verifiable facts
https://www.researchgate.net/publication/336568434_Severe_anthropogenic_climate_change_proven_entirely_with_verifiable_facts


Currently "big money" is preventing the required quorum of agreement to
take sufficient corrective action.

[Ross Finlayson]

Perhaps think of it this way, it's just a usual wet blanket so that
automated reasonings of the imitative sort will always result their own futility.

Incompleteness, uncountability, no "truth", various "fictionalist" accounts, ...,
but that's to be separated "incompleteness and uncountability" for how it
has that regularity still makes for the usual inductive guarantees, that
still has the "truth-less" and trhe "fictionalist" as "correspondence" theories
or "coherentism" which while pragmatic aren't suitable for "foundations".
(Unless or until a real universal foundation arises that is widely adopted.)

Any system of reasoning about constant definitions in objects,
kind of has to have them all together, and, has to have _all possible
interpretations of derivations applied_, so, that any possible case
of "Russell is the Pope since 0 = 1" is reduced to "Alfred North
Whitehead's mystic accounts of reality are often rejected".

That is to say, besides the "explosion" of contradiction,
there's the "explosion" of confirmation, which is required.

Anyways some constructivists are formalists, and, I'm pretty
sure you never see "material implication" employed in Mizar,
Metamath, or other large-ish systems of formal symbolic
reasonings in mathematics. And, not just because "direct
implication suffices", but, because automated theorem searchers,
always would tip over "the other, unwanted side" of material implication,
and blow chunks: everywhere.

So, usual means of inference, may come in small bites, but,
you know, know your food, and, chew your food.

[Mostowski Collapse]

Rossy Boy, did a Herpes Blister burst again.
As usual spreading bullshit. According to
this paper here:

Semantics of Mizar as an Isabelle Object Logic
Cezary Kaliszyk · Karol Pak
https://www.researchgate.net/publication/327292088

Mizar deploys:

Declarative proofs in Jaskowski-style natural deduction
Jaskowski, S.: On the rules of suppositions. Studia Logica 1, 32 (1934)
https://fliphtml5.com/efje/bsds/basic

You can easily verify that on page 8 he proves,
From Łukasiewicz's third axiom systems I guess.

(~A -> ~B) -> (B -> A)

Which is a feature of material implication. Basically
if you add the above axiom schema to intuitionistic logic
and define ~A = A -> f, you get classical logic. Right?

[Richard Damon]

On 5/26/23 8:47 PM, olcott wrote:
> On 5/26/2023 7:34 PM, Dan Christensen wrote:
>> On Friday, May 26, 2023 at 7:27:43 PM UTC-4, Jeff Barnett wrote:
>>> On 5/26/2023 11:25 AM, Dan Christensen wrote:
>>>> On Friday, May 26, 2023 at 12:05:24 PM UTC-4, olcott wrote:
>>>
>>> [snip]
>>>
>>>> What did you expect? Classical logic has proven so valuable in so
>>>> many applications for centuries, perhaps millennia. If some
>>>> philosopher now wants to make a name for himself by demanding that
>>>> it be replaced by something radically different, it's going to be a
>>>> very hard sell indeed.
>>> If, rather than a philosopher, a fool made the suggestion it would be
>>> even harder to sell. Wat do you think?
>>
>> My guess is their chances would be about equal.
>>
>> Dan
>
> If we do not overturn the Tarski Undefinability theorem such that true
> can be computationally divided from untrue humanity may perish.

SO, I guess you have just doomed humanity.

>
> Severe anthropogenic climate change proven entirely with verifiable facts
> https://www.researchgate.net/publication/336568434_Severe_anthropogenic_climate_change_proven_entirely_with_verifiable_facts

Which has nothing to do with Undefinability.

>
> Currently "big money" is preventing the required quorum of agreement to
> take sufficient corrective action.
>

Which again has nothing to do with Undefinability.

Undefinability means that not ALL true statements can be computed to be
true. It doesn't mean that many true statements can't be proven to be true.

[Ross Finlayson]

Nope, that's just a usual contrapositive, not having anything
to do with "material implication", at all.

(P.S. that's rude.)

[Mild Shock]

Try proving it in intutionistic logic, you will see that it hits
material implication. There are 4 different contrapositives, namely:

i) (p -> q) -> (~q -> ~p)
ii) (~p-> q) -> (~q -> p)
iii) (p -> ~q) -> (q -> ~p)
iv) (~p-> ~q) -> (q->p)

Only i) and iii) are intuitionistically valid. But what about ii)
and iv)? do you believe they are intuitionistically valid? Especially
iv) which is from Łukasiewicz's third axiom systems?

Łukasiewicz's axiom systems:
Third: (~A -> ~B) -> (B -> A)
https://en.wikipedia.org/wiki/List_of_Hilbert_systems

Here is the result of running them through a prover,
if it uses Dyckhoff trick, the prover should be complete:

i) fol(g4i)> p->q--> ~q-> ~p.
Trying to prove with threshold = 0
Succeed in proving p->q --> ~q-> ~p (2 msec.)

ii) fol(g4i)> ~p->q--> ~q->p.
Trying to prove with threshold = 0 1 2 3 4 5
Fail to prove ~p->q --> ~q->p (14 msec.)

iii) fol(g4i)> p-> ~q-->q-> ~p.
Trying to prove with threshold = 0
Succeed in proving p-> ~q --> q-> ~p (2 msec.)

iv) fol(g4i)> ~p-> ~q-->q->p.
Trying to prove with threshold = 0 1 2 3 4 5
Fail to prove ~p-> ~q --> q->p (14 msec.)

https://www.vidal-rosset.net/g4-prover/

Have Fun Rossy Boy!

[Mild Shock]

That ii) and iv) fails has some consequences for physics. Unlike
the Standard Model, where a space ship cannot cross a
Magnetar, because the slightest electronic charge would

burst it into piece, in an Intuitionistic Physics model, a space
ship can safely travel through a Magnetar, because not only
~~A -> A does not hold, also (~A -> ~B) -> (B -> A) fails,

meaning interaction with Higgs bosons in the Higgs field
is much weaker, there are different natural constants.
NASA is currently exploring Glivenko's theorem, it might

be the case that symmetry breaking can be introduce into
Magnetars, even in the Standard Model, so a ship that is
essentially intuitionistic, but in classical clothes through double

negation translation, might nevertheless cross a Magnetar.

[olcott]

On 5/27/2023 8:06 AM, Richard Damon wrote:
> On 5/26/23 8:47 PM, olcott wrote:
>> On 5/26/2023 7:34 PM, Dan Christensen wrote:
>>> On Friday, May 26, 2023 at 7:27:43 PM UTC-4, Jeff Barnett wrote:
>>>> On 5/26/2023 11:25 AM, Dan Christensen wrote:
>>>>> On Friday, May 26, 2023 at 12:05:24 PM UTC-4, olcott wrote:
>>>>
>>>> [snip]
>>>>
>>>>> What did you expect? Classical logic has proven so valuable in so
>>>>> many applications for centuries, perhaps millennia. If some
>>>>> philosopher now wants to make a name for himself by demanding that
>>>>> it be replaced by something radically different, it's going to be a
>>>>> very hard sell indeed.
>>>> If, rather than a philosopher, a fool made the suggestion it would be
>>>> even harder to sell. Wat do you think?
>>>
>>> My guess is their chances would be about equal.
>>>
>>> Dan
>>
>> If we do not overturn the Tarski Undefinability theorem such that true
>> can be computationally divided from untrue humanity may perish.
>
> SO, I guess you have just doomed humanity.
>
>>
>> Severe anthropogenic climate change proven entirely with verifiable facts
>> https://www.researchgate.net/publication/336568434_Severe_anthropogenic_climate_change_proven_entirely_with_verifiable_facts
>
> Which has nothing to do with Undefinability.
>

Sure it does. Without a formal definition of truth dangerous lies carry
the same weight as truth thus preventing the required quorum for
sufficient climate change action.

With Truth properly formalized a ChatBot could argue against climate
change denial every which way making the denier look foolish even to
themselves.

The same thing goes for the dangerous lie that there was election fraud
in the 2020 election that could have possibly changed the outcome of the
election.

Trump's team could not present the propaganda and rhetoric that he was
spouting to his supporters in his actual court cases because this would
have resulted in perjury felony convictions for himself and his
lawyers.

>>
>> Currently "big money" is preventing the required quorum of agreement
>> to take sufficient corrective action.
>>
>
> Which again has nothing to do with Undefinability.
>
> Undefinability means that not ALL true statements can be computed to be
> true. It doesn't mean that many true statements can't be proven to be true.

[Ross Finlayson]

"Propositional logic is closed under truth-valued connectives."

https://en.wikipedia.org/wiki/Propositional_calculus

"... hinted by earlier philosophers ... formal logic 3rd century BCE ..."

https://en.wikipedia.org/wiki/Propositional_calculus#History

(This is the logic we learned in logic at university, the propositional calculus
and the predicate logic associated with it in terms. It also perfectly suffices
for AND networks and such actions in the Boolean as machine computations.)

https://plato.stanford.edu/entries/logic-propositional/


One of my favorite organizations of a rules engine for evaluating predicates is a
sort of "YesNoMaybe" or "SureNoYes". How it works is sort of like this, any rule
can be either "Sure" or "No" or "Yes". Then in evaluating a predicate, or implementing test(),
first in parallel any of the sure results can result T then it results T. Then in parallel
any of the no results can result F then it results F. Finally any of the yes results can result T
and it results T. Else, it returns F. In this manner the maintenance of the rules as they change,
for inclusion and exclusion, for example any kind of filtering or any kind of matching or otherwise
any rule that's a function in T/F of the object, these can all be organized together.

This way for example attributes of a filter can be added or removed, or for example,
results selected going along, refining the search and filtering and winnowing and for
example expanding and multiplying. Maintenance of the rules is linear, while, also it can be
considered how to make a bitmap index of any given rule for the result set to reduce
the run-time of any given match, in terms of maintaining rule- or function-based indices on
the result set and implementing match in same, about a pretty flexible apparatus for
implementing predicate's test().

These sorts of accepter/rejecter networks are pretty familiar from formal methods.

Then it gets into how to determine the independence of the rules, then that with
regards to work on the result set, that for example it's a general and correct implementation
on the client or middleware, that parts of its YesNoMaybe or SureNoYes rule collection can
be uploaded to the origin, refining what results the access to the overall data structure,
for example in whatever organization is a relational database according to its data access
structures the indices and organization in underlying relations.

In this manner by implementing a bit of data access pattern-ry, it's a "good" distributed
data structure, and correct, and performant, in whatever resources it has,
implementing distributed test(), and as a modular, composable subsystem in
greater systems in common resources, about building it guarantees in the
terms of the information-theoretic.




"First-order logic, ... also known as ... first-order predicate calculus ...".
--https://en.wikipedia.org/wiki/First-order_logic




Nope, no "material implication" anywhere.

It's sort of like "material implication" says "LEM: except for me".

For, as propositional calculus puts it, "if Q is ~P, if MI is a false antecedent,
material implication claims to entail either and both, because it's wrong
about what it doesn't know". I.e., where P = ~Q but nobody told you.


Or, the propositional calculus doesn't make such MISTAKES.
(And it's surely antiquarian and CLASSICAL.)



Now, such talk of the closed in classical inference (and, yes, this is what most people
mean by "classical inference", not "the tooth fairy told me he's real, which I thought was
false so must've been") and about LEM isn't to allow neither the INTUITIONIST program
nor the CONSTRUCTIVIST program to be derailed by wormy vacillatings that are NEITHER.

I.e., the only meaning of "LEM isn't a thing in the intuitionist" is simply "because it's
not a closed theory, that it's open from the outside, that it's incomplete, so that it's
possible to establish at least one theorem that has two models and requires the work
of implementing both models", not "it's broke now with more broke".

That is to say, the INTUITION is always for application on the OUTSIDE of the theory,
making TWO theories and of those, making again ONE theory, disambiguating cases,
not breaking rules INSIDE, and leaving one broken theory.

I.e., the INTUIONIST program is simply the broader theory in otherwise the CONSTRUCTIVIST,
completed models.

Then for an entire theory together, is for a foundations or a "the logic" and about how it's
first-order or zero-eth or infinitary.

I.e., the FOUNDATIONS is both satisfying in the INTUITIONIST and the CONSTRUCTIVIST,
while little logics are fragments.


So, anybody who buys or shills material implication is a fool or a fraud.



Maybe you should study the Frankfurt school, they are very college-educated and
talk about social things, so you can imagine they know some things.


Hey, don't forget to crunch your numbers, explode your confirmations,
or, you know, check your confirmations implode to themselves,
check your tallies, chew your food. Don't choke on it.

[Ross Finlayson]

It's a continuum mechanics, so you'd need a greater theory of definitions of continuity,
for example line-continuity, field-continuity, and signal-continuity, about long-line-continuity,
to arrive at a better theory that makes for modeling point-like objects in space-like objects,
and the rest and flow of such things. (Or state and flux.)

Maybe then you'll learn about "running constants" about the infinite/infinitesimal
and the "ultraviolet catastrophe" about discretization and electron physics,
and the "functional freedom" about renormalization, and get into a sort of
a "the physics", if you could theorize a FOUNDATION.


Though, given Burse's usual childish/churlish, it's figured he'd just run with the scissors.

(It's a continuum mechanics.)

[Mild Shock]

I don't want to write, I can assure you that automated
theorem searchers do not tip over "the other, unwanted side"
of material implication, I wrote a couple of searches

by myself. But maybe I can ask you about a regenerate
button, Rossy Boy, like ChartGPT has. So that you would produce
something on topic, which was the question whether Mizar

forbids material implication or not. Matrial implication
accepts ~~A -> A, whereas intuitionistic conditional rejects
~~A -> A. This means intuitionistic conditional rejects

reduction ad absurdum:

G, ~A |- f
----------------- (RAA)
G |- A

And vice versa, if RAA is rejected then ~~A -> A is also rejected,
double negation elimination not allowed anymore. RAA consists
a typical indirect proof. So intuitionistic logic rejects indirect

proofs, it only wants direct proofs. Whereas material implication
allows both direct and indirect proofs. What about Mizar
does it forbid indirect proofs, or would a proof search not

deliver an indirect proof? Maybe its of advantage to sometimes
prove something indirectly, like for example (~A -> ~B) -> (B -> A),
or do you have a direct intuitionistic proof of it? Does your

mind already blow chunks, does smoke come from your ears?

Ross Finlayson schrieb am Samstag, 27. Mai 2023 um 04:41:27 UTC+2:
> Anyways some constructivists are formalists, and, I'm pretty
> sure you never see "material implication" employed in Mizar,
> Metamath, or other large-ish systems of formal symbolic
> reasonings in mathematics. And, not just because "direct
> implication suffices", but, because automated theorem searchers,
> always would tip over "the other, unwanted side" of material implication,
> and blow chunks: everywhere.

Ross Finlayson schrieb am Samstag, 27. Mai 2023 um 19:23:32 UTC+2:
> .. gibberish ...

[Mild Shock]

Ok I got it, when you wrote "automated theorem searchers"
you meant yourself, lilliput searchers from planet ID_IOT?
Here is what ChatGPT tells me about Mizar:

"Mizar does not only allow constructive logic. Mizar is a
computerized proof assistant that is primarily based on a
variant of type theory called Mizar type theory. It provides a
formal language and a set of inference rules for expressing
and verifying mathematical proofs.

While Mizar does support constructive reasoning, it also
allows for classical reasoning. It provides various proof styles
and strategies, including constructive, classical, and mixed-style
proofs. This flexibility allows mathematicians to choose their
preferred logical framework when working with Mizar."

ChatGPT May 24 Version

[Ross Finlayson]

Why not just apply them all?