X-Received: by 2002:ac8:6112:: with SMTP id a18mr8211322qtm.401.1637688655780;
        Tue, 23 Nov 2021 09:30:55 -0800 (PST)
X-Received: by 2002:a05:6808:199c:: with SMTP id bj28mr4222542oib.98.1637688654776;
 Tue, 23 Nov 2021 09:30:54 -0800 (PST)
Path: ...!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.logic
Date: Tue, 23 Nov 2021 09:30:54 -0800 (PST)
In-Reply-To: <0898cee2-dc4d-43bc-ad87-ab5ebf53daa2n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <296cf029-1c03-4cc7-a39d-a71a6817516dn@googlegroups.com>
 <723f35b8-6a25-42d8-b209-3694309fe64bn@googlegroups.com> <10f7b843-dad8-49a2-9945-4bf982b00e92n@googlegroups.com>
 <b63adc30-96b1-4da1-a75e-bf3718829d5en@googlegroups.com> <ec44bbea-8c01-4345-b62d-dbe42744b390n@googlegroups.com>
 <d5e68d36-c54f-44e8-a3fd-37b0dbddd4d8n@googlegroups.com> <0898cee2-dc4d-43bc-ad87-ab5ebf53daa2n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <1c47225d-6b96-4c04-acb8-f66d88584dc2n@googlegroups.com>
Subject: Re: DC Proof is the biggest teaching mistake
From: Dan Christensen <Dan_Christensen@sympatico.ca>
Injection-Date: Tue, 23 Nov 2021 17:30:55 +0000
Content-Type: text/plain; charset="UTF-8"
Bytes: 3704
Lines: 72

> Dan Christensen schrieb am Dienstag, 23. November 2021 um 03:17:05 UTC+1:
> > On Monday, November 22, 2021 at 7:45:07 PM UTC-5, Mostowski Collapse wrote:
..
> Mathematics proves things like, using some
> foundational axioms. Thats standard routine:
>
> 3) EXIST(f):Dedekind(f)
>

Again, I proved:

ALL(x):ALL(f):[Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
..
=> EXIST(n):EXIST(x0):[Set(n)
& ALL(a):[a in n => a in x]
& x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n] => [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]
..
This universal generalization is a theorem, and the last line of my proof.
..
Formal proof here: https://dcproof.com/ConstructN.htm
..
The first line is the premise:
..
1 Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
..
The first statement could just as easily have been introduced it as an axiom. It's up to the user.

If the first statement was introduced as an axiom, then the first line would be:

EXIST(x):EXIST(f):[Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

In words, there exists a Dedekind infinite set.

Then the last line would be this theorem:

EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n]
=> [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]

In words, there exists a set on which the Peano axioms hold.

> You are only too lazy, but say it has to do with empty
> domain. But in fact it doesn't have anything to do with
> empty domain.
>

That makes no sense, Jan Burse. Sorry.

Dan

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