DC poop breakthrough: dark booleans spotted on conic sections

[Mostowski Collapse]

*** Breaking News ***
The La Plata Astronomical Observatory Report
*** Breaking News ***

Dan-O-Matik suggests that certain points on a hyperbola
are indeterminate. So that we cannot decide whether they
lie or do not lie on the curve.

Is it possibly that Dan-O-Matik has now shed more lights
on WM dark numbers, in that he has ultimately found dark
booleans? N_def from WM would then be N with

dark boolean membership? I guess this would explain
why AP brain fartos ellipses became ovals, when he entered
his kitchen, possibly there is too much dark boolean

in his kitchen. Lets further dig into the problem. This
parametric plot shows one branch of hyperbola:

https://www.wolframalpha.com/input/?i=parametric+plot+%28cosh%28t%29%2C+sinh%28t%29%29

This is the same hyperbola when we rotate it by 45° degree:

https://www.wolframalpha.com/input/?i=parametric+plot+%28%28cosh%28t%29%2Bsinh%28t%29%29%2Fsqrt%282%29%2C+%28cosh%28t%29-sinh%28t%29%29%2Fsqrt%282%29%29

Is there some parameter t and/or some other branch, so that
we possibly reach the point (0,1) on the plane. Or is the point (0,1)
necessarily never reached? Just flyby by the hyperbola?

[Dan Christensen]

On Sunday, December 5, 2021 at 2:26:31 PM UTC-5, Mostowski Collapse wrote:
> *** Breaking News ***
> The La Plata Astronomical Observatory Report
> *** Breaking News ***
>
> Dan-O-Matik suggests that certain points on a hyperbola
> are indeterminate.

Contrary to what the crank, Jan Burse, here may think, the reciprocal function for the real numbers can be unambiguously defined as f such that:

ALL(x):ALL(y):[x in R & y in R => [x=/=0 => [f(x)=y <=> x*y=1]]]

He believes, but apparently cannot prove that f(0)=1 is false. He just doesn't seem to understand that, since f(0) is undefined, the truth value of f(0)=/=1 is indeterminate. f(0)=/=1 is unprovable. He apparently cannot tell the difference. Oh, well...

Dan

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

[Mostowski Collapse]

Can you go back and forth 45° rotation with your definition?
You know a 45° rotation is a bijection. And with bijection we
are back to beginner math. If you biject two function graphs

A and B, by the bijective function:

h : A -> B, h bijection

Then you can check x e B , by checking h^(x) e A. Does your
claim f(0)≠1 unprovable still hold when you 45° rotate?

[Dan Christensen]

On Sunday, December 5, 2021 at 4:36:55 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 5. Dezember 2021 um 22:04:05 UTC+1:
> > On Sunday, December 5, 2021 at 2:26:31 PM UTC-5, Mostowski Collapse wrote:
> > > *** Breaking News ***
> > > The La Plata Astronomical Observatory Report
> > > *** Breaking News ***
> > >
> > > Dan-O-Matik suggests that certain points on a hyperbola
> > > are indeterminate.
> > Contrary to what the crank, Jan Burse, here may think, the reciprocal function for the real numbers can be unambiguously defined as f such that:
> >
> > ALL(x):ALL(y):[x in R & y in R => [x=/=0 => [f(x)=y <=> x*y=1]]]
> >
> > He believes, but apparently cannot prove that f(0)=1 is false. He just doesn't seem to understand that, since f(0) is undefined, the truth value of f(0)=/=1 is indeterminate. f(0)=/=1 is unprovable. He apparently cannot tell the difference. Oh, well...
> >

> Can you go back and forth 45° rotation with your definition?
> You know a 45° rotation is a bijection. And with bijection we
> are back to beginner math. If you biject two function graphs
>
> A and B, by the bijective function:
>
> h : A -> B, h bijection
>
> Then you can check x e B , by checking h^(x) e A. Does your
> claim f(0)≠1 unprovable still hold when you 45° rotate?

Umm... Is this suppose to somehow prove the that f(0)=1 is false????

Save yourself the embarrassment and just admit that f(0)=/=1 is unprovable since f(0) is undefined.

Dan

[Mostowski Collapse]

A is the conic section: x^2 - y^2 = 1. conic section hyperbola
Which can be parametrically plotted (one branch) by:

parametric plot (cosh(t), sinh(t)): conic section hyperbola
https://www.wolframalpha.com/input/?i=parametric+plot+%28cosh%28t%29%2C+sinh%28t%29%29

You can also verify cosh(t)^2 - sinh(t)^2 = 1 <=> true
https://www.wolframalpha.com/input/?i=cosh%28t%29^2+-+sinh%28t%29^2+%3D+1

Now lets do a rotation 45° by h : A -> B, by sending
(x,y) -> ((x-y)/sqrt(2), (x+y)/sqrt(2))

parametric plot ((cosh(t)-sinh(t))/sqrt(2), (cosh(t)+sinh(t))/sqrt(2)) rectangular hyperbola
https://www.wolframalpha.com/input/?i=parametric+plot+%28%28cosh%28t%29-sinh%28t%29%29%2Fsqrt%282%29%2C+%28cosh%28t%29%2Bsinh%28t%29%29%2Fsqrt%282%29%29

So what is the algebraic curve? Well the back rotation
h^(-1) : B -> A is simply, you can check h^(-1)(h(p)) = p:

(x,y) -> ((x+y)/sqrt(2), (-x+y)/sqrt(2))

Plug in the back rotation into the conic sectio: x^2 - y^2 = 1,
and you get:

((x+y)/sqrt(2))^2 - ((-x+y)/sqrt(2))^2 = 1

Which is equivalent to: x*y = 1/2. rectangular hyperbola
So we can ask f(0)=1 by using h^(-1), where f(x)=1/(2*x).

What will be the result?

[Mostowski Collapse]

Ok, lets rotate the point (0,1) back, we get:
(0+1)/sqrt(2), (-0+1)/sqrt(2)

Or equivalently, a point on the diagonal:
1/sqrt(2), 1/sqrt(2)

Now lets solve the conic section: x^2 - y^2 = 1
g(x) = sqrt(x^2 - 1) = y

Now we have x = 1/sqrt(2),
g(1/sqrt(2)) = sqrt(-1/2)

No real solution.

Ok lets take another point (0,2):
g(2/sqrt(2)) = sqrt(1) = 1

For the x axis x=2/sqrt(2), we would get y=1,
but the point is supposed to be at y=2/sqrt(2).

So also outside of the curve.

[Mostowski Collapse]

Conclusion:

conic section hyperbola
- Like the 45° diagonal through the origin
never intersects with x^2 - y^2 = 1
rectangular hyperbola
- The vertical through the origin
never intersects with x*y = 1

So ~F(0,1), since (0,1) is a point on the vertical through the origin.

[Dan Christensen]

Here is a related question for you, Jan Burse: In an indexed array of 10 Boolean variables, what is the truth value of the 11th one? Duh...

[Mostowski Collapse]

Check wikipedia, F : P -> Q, requires necessarely F ⊆ P x Q:

ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)]

Now take contraposition you get:

ALL(a):ALL(b):[~P(a) | ~Q(b) => ~F(a,b)]

Or in words, if (a,b) is outside of the domain and co-domain, then F is false.

https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

[Mostowski Collapse]

Here is a challenge for DC Proof.

My father thinks
Everybody who thinks exists
----------------------------------------------------
My father exists

Can this be proved in DC Proof?

[Mostowski Collapse]

Or maybe this example:

I think
Whatever thinks exists
----------------------------------------------------
I exist

Takle it with the maybe monad. With an
ordinary quantifer, everything works fine:

I encode x exists as ∃y(some(y)=x).
We can then prove:

(Ti ∧ ∀x(Tx → ∃ys(y)=x)) → ∃ys(y)=i is valid.
https://www.umsu.de/trees/#Ti~1~6x%28Tx~5~7y%28s%28y%29=x%29%29~5~7y%28s%28y%29=i%29

Now change the forall quantifier to the
Dan-O-Matik forall quantifier:

(Ti ∧ ∀x(Ts(x) → ∃ys(y)=s(x))) → ∃ys(y)=i is invalid.
Countermodel:
Domain: { 0, 1 }
i: 0
s: { (0,1), (1,1) }
T: { 0 }
https://www.umsu.de/trees/#Ti~1~6x%28Ts%28x%29~5~7y%28s%28y%29=s%28x%29%29%29~5~7y%28s%28y%29=i%29

He He, cool!

[Mostowski Collapse]

Lets say a quantifier of this definition would be the
little brother of the Dan-O-Matik quantifier:

/* Maybe Quantifier */
ALL(x):P(x) :<=> ∀xP(some(x))

In Isabelle/HOL etc.. the option type is a polymorphic
type. So for each sort a , there some sort option(a).
What would happen if we are in the ZFC universum.
We could model option(V) as follows:

Isabelle/HOL. ZFC
none {}
some(x) {x}

So we would encode option(V) inside V itself. We could
then create a new Peano Apostroph:

/ {y} for ∃!z(x,z) e F & (x,y) e F
F'x = <
\ {} for ~∃!z(x,z) e F

We could also provide an alternative Set(_) predicate.
Alternative to what Dan-O-Matik does. Set would be a
predicate over option(V), and could be defined as follows:

Set(x) <=> ∃y({y}=x)

So Set(_) would be the non-emptyness predicate in
the sense of free-logic.

Hm...

P.S.: We could use this in yet another Peano apostroph:

/ {y} for ∃!z(∃t({t}=x) & (t,z) e F) & ∃t({t}=x) & (t,y) e F
F'x = <
\ {} for ~∃!z(∃t({t}=x) & (t,z) e F)

So the graph would be still F ⊆ V x V, but the Peano apostoph
provides a view one some F' ⊆ V x option(V). Not only
would the Peano apostroph make the codomain option(V),

but it would also make decision in the domain, depending
on whether an argument x is in option(V) \ {} or not. So
we could then prove:

∀x(~Set(x) => ~Set(F'x))

[Mostowski Collapse]

So you didn't do regression testing of your changes?
DC Proof is not a reliable to tool. It nowhere automatically
records in the generated HTML files the version of DC Proof.

For example in the link
http://www.dcproof.com/ProofByInduction.html
I find:

Apply definition of n for f(x)

30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 11

What is the f(x) e S before line 30? I suspect it is not
an U Spec from dcproof5.exe with two reference
lines, it has only one reference line 11.

LoL

[Mostowski Collapse]

Alternatively instead of only posting HTML, you could
also post additionally a link to the machine readable
proof, so that one can load it into DC Proof,

and verify that then proof goes through. All tools
such as Isabelle/HOL, Coq, etc.. have such a format,
and publishing a proof means publishing this

format and not some pretty printing. Although
in Isabelle/HOL, Coq, etc.. the format is very simple.
Mostlikely ASCII, maybe recently Unicode,

but not binary. The pretty printing is then often
LaTex or HTML. You only post pretty printing, nobody
can verify, with a press of a button, what you did.

[Mostowski Collapse]

Your Dedekind -> Peano proof doesn't work anymore.
Its the same problem like in this proof, where
this step doesn't work anymore:

> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
> [...]
> 8 ~Field(constr(a))
> U Spec, 6, 7
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

Because there is no constr(a) e S.

The new error message is:
'constr(a)' must be an element of a set

[Dan Christensen]

See my reply just now to your identical posting at sci.math

Dan

[Mostowski Collapse]

Did you make you proof with the help of a pendulum
or what. Did you also find some water? LoL

Here is a simple proof, assume it ends with,
two alternatives 1) or 2) for demonstration:

1) ALL(x):[egg(x) => hatch(x,chicken(x))]
2) ALL(x):[egg(x) => EXIST(y):hatch(x,y)]

Can you now prove? No, none is provable:

1) => 3) EXIST(x):[egg(x) & hatch(x,chicken(x))]
2) => 4) EXIST(x):[egg(x) & EXIST(y):hatch(x,y)]

You didn't show that a Peano chicken exists.
We don't know whether there are some Dedekind eggs.

On the other hand Zermelo did it correctly.

Got it Bozo?

[Dan Christensen]

See my reply just now to your identical posting at sci. math

[sergio]

a man has two legs
a monkey has two legs
therefore all men are monkeys

[Mostowski Collapse]

Students beware of fake DC Proof. There is one more
problem with DC Proof, and its not my fault.
Dan-O-Matik himself started comparing his Peano

nonsense with set theory, and in particular with
Zermelos axiom of infinity, which states the existence
of an inductive set. So what is a further "bug" in

Dan-O-Matiks comparison? Zermelo proves more!
Zermelo proves global derived existence of omega, wheras
Dan-O-Matik only shows local derived existence of a Peano

structure. See yourself:

Dan-O-Matik, only derived local existence:
ALL(f):[Dedekind(f) => EXIST(n):Peano(f,n)]

Zermelo, derived global existence:
EXIST(w):ALL(s):[Inductive(s) => Omega(s,w)]

But Zermelo must also add EXIST(s):Inductive(s),
because without it, deriving existence
doesn't work out directly from his theorem:

∃w∀s(Is → Osw) → ∃s∃wOsw is invalid.
Countermodel:
Domain: { 0 }
I: { }
O: { }
https://www.umsu.de/trees/#~7w~6s%28Is~5Osw%29~5~7s~7wOsw

Would be similar fallacy. Similar cure though:

(∃sIs ∧ ∃w∀s(Is → Osw)) → ∃s∃wOsw is valid.
https://www.umsu.de/trees/#~7sIs~1~7w~6s%28Is~5Osw%29~5~7s~7wOsw

[Mostowski Collapse]

We can also show uniqueness, replacing ∃w by ∃!w.
And the parameter s can be eliminated in the definition
of omega, so we can prove in Zermelo:

∃!wOmega(w)

On the other hand in Dan-O-Matik, inside one domain
of discourse, there are many many Peano structures,
for each function f with Dedekind(f) there is a

Peano(f,n). Sometimes if we have f1 and f2, turns
out that the Peano structurs are the same, but there
are also f1 and f2 where the Peano structure is

not the same. Thats quite "unnatural" to have many
different "natural" numbers inside a domain of discourse.
Usually when we talk of natural numbers, such as

1, 2, 3, etc.. we don't assume that suddently there
are further natural numbers 1', 2', 3', etc.. generated
from an other Dedekind function. And so on.

What are Dan-O-Matiks numbers, potato numbers?

[Mostowski Collapse]

Well the core question is why would one need this in
Number Theory? I asked this already a dozen time.
Why does one need your Function Axiom or a

Construction of add, why does one need an add based
on material implication, when Landau can do the
following without it?

Landau can do in FOL=:

∀x ∀y ∃!z (x + y = z)

Landau can do in FOL= with Set-Less Induction Schema:

∀x ∀y (x + y = y + x)

Also you don't show really existence of add, since you
assume Set Induction. But for example in ZFC Set Induction
can itself be shown to exist.

You don't make any sense with your pseudo existence
of add. It needs existence of induction. ZFC on the other
hand can prove induction.

You don't make any sense with your pseudo existence
of add, its not needed for ∀x ∀y ∃!z (x + y = z) and its
not needed for ∀x ∀y (x + y = y + x) .

So your add construction is:
a) False claim, it depens on Induction (unlike a ZFC construction)
b) Not motivated, we still don't know what it is used for,
neither Landau ∀x ∀y ∃!z (x + y = z) nor ∀x ∀y (x + y = y + x)
needs it.

[Mostowski Collapse]

**************************************
Breaking News: A new form of dark matter revealed
**************************************

Like Schrödingers cat, there are now proofs that
exist and don't exist. For example Dan Christensen claims
that he knows (for my ~(m e n) and s(m)=0 example):

~ALL(a):[a e n => ~s(a)=0]

But he cannot prove it. This is a sensation. We
have found Gollums dog!

[Dan Christensen]

See my reply just now to your identical, idiotic posting at sci.math

Dan

[Mostowski Collapse]

Because -1 is not in N, this axiom is still
true, even if s : Z -> Z, thats pretty clear:

4. ALL(a):[a in N => ~s(a)=0]
Axiom

Just substitute a = -1, and you get

-1 e N => ~s(-1)=0

Which is vacously true, because -1 e N is false.
https://en.m.wikipedia.org/wiki/Vacuous_truth

Whats wrong with you? Got it now dumbo?
Never heard of material implication?

[Mostowski Collapse]

Definition of vacously true:

In mathematics and logic, a vacuous truth is a conditional
or universal statement (a universal statement that can be converted
to a conditional statement) that is true because the antecedent
cannot be satisfied.
https://en.m.wikipedia.org/wiki/Vacuous_truth

All your „Peano Axioms“ are of the form ALL(a):[a e N => …]
so they are automatically vacously true for instantiations
with values outside of N.

The are vacously true, and not vacously false as you
think right now. Whats wrong with you?

[Mostowski Collapse]

After Dan Christensen has claimed that:

subst( s, succZ, ALL(a):[a e n => ~s(a)=0] ) =\= ALL(a):[a e n => ~succZ(a)=0]

He thinks it gives ALL(a):[a e z => ~succZ(a)=0],
I am expecting Dan Christensen will soon talk about
ellipses that are oval, just like AP brain farto.

Hail DC 💩 Poop 💩, brain confusion guaranteed.

[Mostowski Collapse]

Why use Wonky nonsense called „ basic arithmetic (line 1-14) “ as here for Even:
https://dcproof.com/EvenNextOdd.htm

Why not use Presburger arithmetic:
https://de.m.wikipedia.org/wiki/Presburger-Arithmetik

You can then define:
Even(x) <=> EXISTS(y):[y+y=x]

And the prove:
Even(x) & Even(y) => Even(x+y)

Basically anything made from eliminable definitions and +
is either provable or refutable, since Presburger is complete.

Not incomplete as your Wonky „ basic arithmetic (line 1-14) “

[Mostowski Collapse]

You can also extend Presburger Arithmetic by notation:

n * x = x + … + x
\ n-times /

You can then more conveniently write:

Even(x) <=> EXISTS(y):[2*y=x]

But you wouldnt introduce arbitrary multiplication,
only a short hand n * x for x + … + x.

[Mostowski Collapse]

STUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math and science
He can even not tell apart intuitionistic logic and other non-classical logic.

He is such a baby concerning non-classical logic. Also his tool DC Poop
cannot do non-classical logics, its too rigid. For example it has double negation

elimination built-in. So it cannot be used to teach students non-classical logic.

[Dan Christensen]

On Thursday, December 22, 2022 at 7:16:02 PM UTC-5, Mostowski Collapse (Jan Burse) wrote:
> STUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math and science
> He can even not tell apart intuitionistic logic and other non-classical logic.
>
> He is such a baby concerning non-classical logic.

The rules of logic built into DC Proof is just the rules of logic used in the vast majority mathematical textbooks. That just seems to drive Jan Burse here crazy. Poor baby.

> Also his tool DC Proof

> cannot do non-classical logics, its too rigid. For example it has double negation
> elimination built-in.

It would be quite useless otherwise. Removing double negations is done routinely in mathematics to no ill effect whatsoever.

> So it cannot be used to teach students non-classical logic.

Just tell them, as as challenge, not use the Remove Double Negation Rule (on the Logic menu) for whatever proof you have in mind. I myself find math challenging enough as it is without such self-imposed restrictions.

[Mostowski Collapse]

What drugs are you consuming Dan-O-Matik? Just
enter (a=>b)=>(~a=>b)=>b here and you get. Note the
associativity of (=>) operator assumed by the stanford tool:

a b ((a → b) → ((¬a → b) → b))
F F T
F T T
T F T
T T T
https://web.stanford.edu/class/cs103/tools/truth-table-tool/

Looks like a classical tautology to me! Why do you think its not a tautology?
Does your stupid DC Proof tool parse P=>Q=>R wrongly. Well we do parse
it as P=>(Q=>R). We told you already that this is a bug in DC Proof.

Time to fix your freaking DC Proof tool.

Dan Christensen schrieb am Freitag, 23. Dezember 2022 um 15:03:50 UTC+11:
> > For mathematics the question of acceptance of ((~A => B)
> > => (A => B) => B), is much more important.
> Wrong again, Jan Burse. This is not a tautology.

[Mostowski Collapse]

If the stanford truth table generator is not enough evidence
for you that P=>Q=>R is commonly parsed as P=>(Q=>R)
try the same with Wolfgang Schwartz tool:

Enter (a=>b)=>(~a=>b)=>b and you get:

(a→b) → ((¬a→b) → b) is valid.
https://www.umsu.de/trees/#(a~5b)~5(~3a~5b)~5b

Same associativity as in the stanford truth table generator.
In Prolog terms the associativity for implication is xfy and
it is not yfx. Got it dumbo? You only create confusion if

you cannot read what other people post and make hillarious
claims about certain formulas not being classical tautologies.

Time to fix your freaking DC Proof tool.

[Dan Christensen]

On Friday, December 23, 2022 at 3:43:19 AM UTC-5, Mostowski Collapse wrote:
> If the stanford truth table generator is not enough evidence
> for you that P=>Q=>R is commonly parsed as P=>(Q=>R)

[snip]

Consistent with all other binary operators, '=>' is left associative in DC Proof.

[Mostowski Collapse]

Coq doesn't have it either your way. Coq does also have:

Page 3:

The notation
a -> b -> c
actually stands for
a -> (b -> c)

https://cel.hal.science/file/index/docid/459139/filename/coq-hurry.pdf

You better fix your nonsense tool DC Poop.

[Mostowski Collapse]

Anyway, Merry Holidays to our Chief Crank Dan Christensen.
Here is some Christmas homework:

- What does it mean when a mathematician writes in
a text book: "We can constructively show ..."

- What does it mean when a mathematician writes in
a text book: "We can non-constructively show ..."

- What does it say that every intuitionistic proof is
also a classical proof, there is this rather trivial
meta-mathematical implication between the two logics:

T |-_I A => T |-_C A

- What does it say that there are classical only proofs, i.e.
that the above meta theorem cannot be reversed,
i.e. that we have some theories T and formulas A:

T |-_C A & ~ T |-I A

[Dan Christensen]

See my reply just now to your identical posting at sci.math

Dan

On Saturday, December 24, 2022 at 8:25:46 PM UTC-5, Mostowski Collapse wrote:
> Coq doesn't have it either your way. Coq does also have:
>
> Page 3:
>
> The notation
> a -> b -> c

> actually stands for ...

[Mostowski Collapse]

STUDENTS BEWARE: Don't be a victim of Dan Christensens's fake math
and science. He is totally clueless concerning counterfactual conditional.
You don't make any sense, why do you list material implication truth tables?

Obviously vacuous truth is not a principle that holds in counterfactual
conditional. Let A => B denote material implication, and let A > B
denote couterfactual conditional:

/* Is a Tautology */
A => (~A => B)

/* is not generally valid */
A > (~A > B)

Whats your prololololoblem? Why do you always list truth tables for
material implication. They wont show couterfactual conditional.
At least not a counterfactual conditional that would

have this definition:

A > B :<=> Bew('A => B')

Where ' ' some Gödel numbering and Bew (german Beweis, english Proof)
is as in Gödels incompletness theorem.

[Dan Christensen]

On Tuesday, January 31, 2023 at 1:28:23 PM UTC-5, Mostowski Collapse wrote:

>[snip childish abuse] ... concerning counterfactual conditional.

> You don't make any sense, why do you list material implication truth tables?
>

The standard truth table for IMPLIES shows, among other things, how the principle of vacuous truth works. In that table, wherever the antecedent is false, the implication is true regardless of the truth value of the consequent.

> Obviously vacuous truth is not a principle that holds in counterfactual
> conditional.

You can use counterfactual conditionals, for example, to speculate about what might have been had unicorns ever existed. AFAICT counterfactuals are useless for presenting any kind of logical argument. At best, they can be used to present an "educated" guess or opinion.

[snip]

> Why do you always list truth tables for
> material implication.

You also seemed to have trouble with the notion of vacuous truth. As I pointed out, if you accept the standard truth table for logical implication, you must also accept the principle of vacuous truth. Deal with it, Mr. Collapse.

[Mostowski Collapse]

And could you solve the riddle why counterfactual conditional
differs from material implication? Not only they are different
names, they also refer to different inference rules.

One inference rule found in strict implication when modelling
A > B as the modal formula [](A => B), is the rule of necessity:

|- C
--------
|- []C

Lets say this is the only inference rule for our counterfactual
conditional. I guess its evident that A > ( ~A > B) isn't provable,

isn't it? Usually Provability logics based on modal operator,
have one more axiom, but this additional axiom will also

not allow derivation of A > ( ~A > B) right?

See also:

Basic Concepts in Modal Logic - Edward N. Zalta
https://www.cs.brandeis.edu/~cs112/cs112-2004/newReadings/ConceptsModalLogic.pdf

Wiki Article - Provability logic
https://en.wikipedia.org/wiki/Provability_logic

[Mostowski Collapse]

This author suggests some Prolog code for modal
logic propositional theorem prover:

6 A Modal Calculus for K
leanTAP Revisited - Melvin Fitting, 1997
http://melvinfitting.org/bookspapers/pdf/papers/LeanTaP.pdf

Could try to provide a theorem prover with A => B and
A > B, and model A > B by [](A => B).

Could be fun!

[Dan Christensen]

On Tuesday, January 31, 2023 at 7:50:21 PM UTC-5, Mostowski Collapse wrote:
> And could you solve the riddle why counterfactual conditional
> differs from material implication? Not only they are different
> names, they also refer to different inference rules.
>

[snip]

Counterfactuals deal with speculation about what might have been--not very useful for reasoning about the present AFAICT. On the other hand, classical propositional logic, including material conditionals, deals with what is actually true in the present. I hope this helps.

[Mostowski Collapse]

What makes you think (A > (~A > B)) should be
derivable for a counterfactual conditional?

[Dan Christensen]

On Wednesday, February 1, 2023 at 5:20:36 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 1. Februar 2023 um 04:11:31 UTC+1:
> > On Tuesday, January 31, 2023 at 7:50:21 PM UTC-5, Mostowski Collapse wrote:
> > > And could you solve the riddle why counterfactual conditional
> > > differs from material implication? Not only they are different
> > > names, they also refer to different inference rules.
> > >
> > [snip]
> >
> > Counterfactuals deal with speculation about what might have been--not very useful for reasoning about the present AFAICT. On the other hand, classical propositional logic, including material conditionals, deals with what is actually true in the present. I hope this helps.

> What makes you think (A > (~A > B)) should be
> derivable for a counterfactual conditional?

What makes you think I do? I don't see the point of formalizing counterfactuals. They amount to a kind of non-logical figure of speech like so many others in natural language.

[Mostowski Collapse]

Chu Space have a charming counterfactual aspect.
Lets define the Set embedding as follows, where U is
the Herbrand Universe, a little diversion from the slides:

[X] = (X, U \ X)
https://bentnib.org/docs/datatypes-with-negation-20220623.pdf

This somehow explains the below non-monotonic example:

:- dynamic abnormal/1.
fly(X) :- bird(X), \+ abnormal(X).
bird(tweety).
?- fly(tweety).
true.

And then:

abnormal(tweety).
?- fly(tweety).
false.

Have Fun!

[Mostowski Collapse]

STUDENTS BEWARE: Don't be a victim of Dan Christensen's fake
math and science. He cannot tell which "=>" Principles are needed to prove:

A & B => [A => B]
A & ~B => ~[A => B]
~A => [A => B]

Or equivalently:

A => [B => [A => B]]
A => [[B => f] => [[A => B] => f]]
[A => f] => [A => B]

LoL

[Dan Christensen]

On Sunday, February 5, 2023 at 6:30:53 PM UTC-5, Mostowski Collapse wrote:
> STUDENTS BEWARE: Don't be a victim of Dan Christensen's fake
> math and science. He cannot tell which "=>" Principles are needed to prove:
>

Grasping at straws as always, Mr. Collapse here continues to embarrass himself.

> A & B => [A => B]
> A & ~B => ~[A => B]
> ~A => [A => B]
>
> Or equivalently:
>
> A => [B => [A => B]]
> A => [[B => f] => [[A => B] => f]]
> [A => f] => [A => B]
>

The rules of logic built into my DC Proof 2.0 program (see the Logic menu on the main screen) are more than sufficient to handle such proofs. It must be frustrating as hell for our Mr. Collapse here.

[Mostowski Collapse]

And which one are needed for:

A => [B => [A => B]]
A => [[B => f] => [[A => B] => f]]
[A => f] => [A => B]

You don't have any rules for f (Falsum) in DC Proof.
Ok, you are allowed to use P & ~P instead. But
then & and ~ inference rules might sneak in again.

I am pretty sure these inference rules are not enough:

> 1. Conditional proof: If you can prove B is true,
> assuming only that A is true, then you can infer that the implication A=>B is also true.
> 2. Detachment (modus ponens): If the implication A=>B is true,
> and A is true, then B must also be true.

Contrary to your claim.

[Dan Christensen]

On Sunday, February 5, 2023 at 7:24:01 PM UTC-5, Mostowski Collapse wrote:
> And which one are needed for:
> A => [B => [A => B]]
> A => [[B => f] => [[A => B] => f]]
> [A => f] => [A => B]

Guessing at your unusual notation here, that you probably meant:

A => [B => [A => B]]

~F =>[ A => [[B => F] => [[A => B] => F]]]
~F => [ [A => F] => [A => B]]

DC Proof should be able to easily handle them. All are tautologies.

[Dan Christensen]

On Sunday, February 5, 2023 at 7:55:12 PM UTC-5, Dan Christensen wrote:
> On Sunday, February 5, 2023 at 7:24:01 PM UTC-5, Mostowski Collapse wrote:
> > And which one are needed for:
> > A => [B => [A => B]]
> > A => [[B => f] => [[A => B] => f]]
> > [A => f] => [A => B]
> Guessing at your unusual notation here, that you probably meant:
> A => [B => [A => B]]
> ~F =>[ A => [[B => F] => [[A => B] => F]]]

Trivial...

1. ~F
Premise

2. A
Premise

3. B => F
Premise

4. A => B
Premise

5. B
Detach, 4, 2

6. ~F => ~B
Contra, 3

7. ~B
Detach, 6, 1

8. ~B => F
Arb Cons, 5

9. F
Detach, 8, 7

10. A => B => F
Conclusion, 4

11. B => F => [A => B => F]
Conclusion, 3

12. A => [B => F => [A => B => F]]
Conclusion, 2

13. ~F => [A => [B => F => [A => B => F]]]
Conclusion, 1

> ~F => [ [A => F] => [A => B]]
>

Left as an exercise for you, Mr. Collapse.

[Dan Christensen]

Recall that, like every other binary infix relation, '=>' is left associated in DC Proof.