Pitty DC Proof cannot do Unicode. I cannot use the Greek φ ?
How annoying. Anyway here is the DC Proof proof. The proof
is a little shorter, I think my gentzen/1 proof search generates

some longer detours because of the way it deals with negation,
since it doesn't directly search shortest natural deduction proof,
but rather works its way through search a Gentzen style proof,

but then manually doing the proof, gives something much shorter.
But can we get rid of the two Rem DNeg, to make it constructive?
Or at least can we get rid of the inner Rem DNeg?

15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14

------------------------------------ begin proof ------------------------------------------

1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise

2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1

3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2

4 ~Phi(u,u) => Phi(u,u)
Split, 3

5 Phi(u,u) => ~Phi(u,u)
Split, 3

6 ~Phi(u,u)
Premise

7 Phi(u,u)
Detach, 4, 6

8 ~Phi(u,u) & Phi(u,u)
Join, 6, 7

9 ~~Phi(u,u)
4 Conclusion, 6

10 Phi(u,u)
Rem DNeg, 9

11 ~Phi(u,u)
Detach, 5, 10

12 Phi(u,u) & ~Phi(u,u)
Join, 10, 11

13 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1

14 ~~ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Quant, 13

15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14

------------------------------------ end proof ------------------------------------------

Mild Shock schrieb am Sonntag, 27. August 2023 um 13:32:08 UTC+2:
> Since we didn't post a proof that wasn't using function
> equality, I started adoption Culios proof in Coq. Now I saw that
> it could be non-constructive, since it uses tauto. But have to
>
> check what tauto does. Culios proof reads:
>
> > (* [exists_h] is "inconsistent". *)
> > Theorem exists_h_to_false :
> > exists_h -> False.
> > Proof.
> > unfold exists_h, het, aut.
> > intros [h H].
> > destruct (H h) as [PN NP].
> > tauto.
> > Qed.
>
> So it starts with unfold, so we can anyway throw away the
> definitions and try directly a proof of the following. Unfortunately
> my only version does have <=> so lets do it with two =>:
>
> ?- gentzen(∀h: ¬ (∀w: ((¬φ(w,w) →φ(h,w))∧(φ(h,w)→ ¬φ(w,w) ))), N), !.
> https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example52/package.html
>
> This is the proof it shows me. It uses Reductio, so its non-
> constructive. Maybe can turn it into a constructive proof?
>
> 1 ∀w:((¬φ(w, w) → φ(u, w)) ∧ (φ(u, w) → ¬φ(w, w)))
> Premise
> 2 (¬φ(u, u) → φ(u, u)) ∧ (φ(u, u) → ¬φ(u, u))
> U Spec 1
> 3 φ(u, u) → ¬φ(u, u)
> Split Right 2
> 4 ¬φ(u, u) → φ(u, u)
> Split Left 2
> 5 ¬φ(u, u)
> Premise
> 6 φ(u, u)
> Premise
> 7 ⊥
> Detach 6,5
> 8 ¬φ(u, u)
> ▲ Conclusion 6,7
> 9 φ(u, u)
> Detach 8,4/
> 10 ⊥
> Detach 9,5
> 11 φ(u, u)
> ▲ Reductio 5,10
> 12 ¬φ(u, u)
> Detach 11,3
> 13 ¬φ(u, u)
> Premise
> 14 φ(u, u)
> Premise
> 15 ⊥
> Detach 14,13
> 16 ¬φ(u, u)
> ▲ Conclusion 14,15
> 17 φ(u, u)
> Detach 16,4
> 18 ⊥
> Detach 17,13
> 19 φ(u, u)
> ▲ Reductio 13,18
> 20 ⊥
> Detach 19,12
> 21 ¬ ∀w:((¬φ(w, w) → φ(u, w)) ∧ (φ(u, w) → ¬φ(w, w)))
> ▲ Conclusion 1,20
> 22 ∀h: ¬ ∀w:((¬φ(w, w) → φ(h, w)) ∧ (φ(h, w) → ¬φ(w, w)))
> U Gen 21

Come look and see, how Rossy Boy looses his marbles:

Ross podcasts talks about mathematics,
physics, science, logic, philosophy
https://groups.google.com/g/sci.math/c/N1YgkTqERJc

"Archimedes Plutonium and Rossy Boy should be thrown in jail
for their willful criminal behavior. The criminals Archimedes
Plutonium and Rossy Boy all the times posts people
name lists together with hate speach about these people.

It is highly likely Archimedes Plutonium and Rossy Boy are
psychos. Archimedes Plutonium and Rossy Boy belong in prison
not on usenet for their mind is complete hate hate hate.
Put these creeps in jail and throw away the keys."

LoL

Ross Finlayson schrieb:
> On Tuesday, August 22, 2023 at 7:57:56 PM UTC-7, Dan Christensen wrote:
>> On Tuesday, August 22, 2023 at 10:09:38 PM UTC-4, Ben Bacarisse wrote:
>>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>>
>>>> On Tuesday, August 22, 2023 at 7:01:09 PM UTC-4, Fritz Feldhase wrote:
>>>>> On Tuesday, August 22, 2023 at 8:01:09 PM UTC+2, Dan Christensen wrote:
>>>>>
>>>>>> Functions f and g are comparable only if they have the same domain
>>>>>> and codomain.
>>>>>
>>>>> Anyone except crank DC knows that this is nonsense.
>>>>
>>>> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
>>>> g : X → Y with the same domain and range [codomain] are said to be equal, f = g,
>>>> if and only if f(x) = g(x) for all x ∈ X. "
>>>> ---Terence Tao, "Analysis I," p.51 (Perhaps you have heard of him?)
>>> Tao does not support your claim. For example (from the same book):
>>>
>>> "... the two functions f and g are not considered the same function,
>>> f =/= g, because they have different domains."
>>>
>> Some context:
>>
>> "Strictly speaking, there is a distinction between a function f, and its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f|[1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains. Despite this distinction, we shall often be careless, and say things like 'consider the function x^2 + 2x + 3' when really we should be saying 'consider the function f : R → R defined by f(x) := x^2 + 2x + 3'”.
>> --p. 218
>>
>> It would disingenuous to suggest that this discussion of liberties often taken in the literature is somehow a repudiation of his formal definition of the equality of functions. "[W]e shall often be careless, and say things like..."
>> Dan
>>
>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>
> Function theory is among the most overloaded of the fields of elementary kinds of objects,
> over time.
>
> It's as of matters of relations, where relations are about being more fundamental than predicates,
> even though usually enough it's the other way way. Other usual examples includes integers
> then rationals or integers in rationals, where intensionality and extensionality get reversible
> because they are reversible because there's a geometry of points and spaces for the most of
> the assignments of the mathematical objects and it's reversible.
>
> Now, coming from a guy like Dan who says "I proved 0^0 = 1", and it's like no you didn't, you
> picked a branch of a multiplicity as what was a singularity to make a regularity and your
> restriction of comprehension is noted as simply a letting, to "let", something be, that's
> otherwise it's just another usual sort of wishful thinking. Because, for example, otherwise
> you'd accept there aren't negative numbers, there aren't complex numbers, and so on,
> just like other usual retro-finitist trolls of the sourpuss, folderol, and jibing ape variety.
>
>