Is this a correct statement of Zorn's Lemma?

[Dan Christensen]

I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma

Is the following a correct statement of Zorn's Lemma?

Where

Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y


ALL(s):[Set(s)

& EXIST(a):a in s (s is non-empty)

& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)

& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)

=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)


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]

To model a partially ordered set, you
need to use a pair <P,=<> with P a set and

=< subset PxP. Otherwise this gets you nowhere
using a predicate. Because you need to treat =<

as a set. If =< is not a set, you also don't
know whether this here { x | y =< x } is a set,

and so on. And then you cannot apply the
axiom of choice.

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
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]

Maybe you can workaround it, and use
a predicate nevertheless, if you state

somewhere:

forall x,y (x=<y => x e P /\ y e P)

Which says =< subset P x P.

Post by Mostowski Collapse
To model a partially ordered set, you
need to use a pair <P,=<> with P a set and
=< subset PxP. Otherwise this gets you nowhere
using a predicate. Because you need to treat =<
as a set. If =< is not a set, you also don't
know whether this here { x | y =< x } is a set,
and so on. And then you cannot apply the
axiom of choice.

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
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]

Post by Mostowski Collapse

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

To model a partially ordered set, you
need to use a pair <P,=<> with P a set and
=< subset PxP.

I "model" <= on the set s as follows:

1. ALL(a):[a in s => a<=a] (reflexity of <=)

2. ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)

3. ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)


<= could be ANY partial order on S.

Post by Mostowski Collapse
Otherwise this gets you nowhere
using a predicate. Because you need to treat =<
as a set. If =< is not a set, you also don't
know whether this here { x | y =< x } is a set,
and so on. And then you cannot apply the
axiom of choice.

If needed, I could construct the subset of {(x,y) in SxS : x<=y}


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]

You forgot to repeat reflexity, antisymmetry
and transivity for the subsets. You only
state that the subset has "connexity".

But =< must be a partial order on S.

And =< must be a partial order on each
subset B as well, and =< must be connex
on each subset B.

You can check yourself:
The term chain is a synonym for a totally
ordered set, but the term is often used to
mean a totally ordered subset of some
partially ordered set, for example
in Zorn's lemma.
https://en.wikipedia.org/wiki/Total_order#Chains

totally ordered = partial order + connex

You can spare repeating reflexivity
for the subsets B, since The connex property
also implies reflexivity, i.e., a ≤ a.

Post by Dan Christensen

Post by Mostowski Collapse

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

To model a partially ordered set, you
need to use a pair <P,=<> with P a set and
=< subset PxP.

1. ALL(a):[a in s => a<=a] (reflexity of <=)
2. ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
3. ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
<= could be ANY partial order on S.

Post by Mostowski Collapse
Otherwise this gets you nowhere
using a predicate. Because you need to treat =<
as a set. If =< is not a set, you also don't
know whether this here { x | y =< x } is a set,
and so on. And then you cannot apply the
axiom of choice.

If needed, I could construct the subset of {(x,y) in SxS : x<=y}
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Mitch Raemsch]

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On the Zorns of a dilemma...?

[FromTheRafters]

Post by Mitch Raemsch

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No
promises!) There is some ambiguity in the Wikipedia article at
https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]]
(antisymmetry of <=) & ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s
=> [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <=
in a) => EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness
of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On the Zorns of a dilemma...?

Ha, Mitch made another joke.

[Archimedes Plutonium]

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at

AP writes:: bypass the worthless goonclod failure of math and logic and learn some real math from the master -- AP



3-1
TEACHING TRUE MATHEMATICS: journal-textbook for ages 5 to 18, Volume 1; textbook math series, book 1 Kindle Edition
by Archimedes Plutonium (Author)


3-2
TEACHING TRUE MATHEMATICS: Volume 2 for age 18-19, 1st year College Calculus, math textbook series, book 2 Kindle Edition
by Archimedes Plutonium (Author)

3-3
COLLEGE CALCULUS GUIDE to help students recognize math professor spam from math truth & reality//textbook math series, book 3 Kindle Edition
by Archimedes Plutonium (Author)


3-4
TEACHING TRUE MATHEMATICS: Volume 3 for age 19-20 Sophomore-year College, math textbook series, book 4 Kindle Edition
by Archimedes Plutonium (Author)

3-5
TEACHING TRUE MATHEMATICS: Volume 4 for age 20-21 Junior-year of College, math textbook series, book 5 Kindle Edition
by Archimedes Plutonium 2019


3-6
TEACHING TRUE MATHEMATICS: Volume 5 for age 21-22 Senior-year of College, math textbook series, book 6 Kindle Edition
by Archimedes Plutonium 2020

3-7
TEACHING TRUE MATHEMATICS: Volume 6 for age 22-26 Graduate school, math textbook series, book 7 Kindle Edition
by Archimedes Plutonium 2020

[Dan Christensen]

Post by Archimedes Plutonium

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at

AP writes:: bypass the worthless goonclod failure of math and logic and learn some real math from the master -- AP

WARNING TO STUDENTS: Don't be a victim of AP's fake math and science

AP is a malicious troll who really, REALLY wants you to fail in school just like he must have so long ago (in the 1950's or 60's?). Then he would like to recruit you to his sinister Atom God Cult of Failure. Think I'm making this up? IN HIS OWN WORDS:


AP's fake math that can only be designed to promote failure in schools:

“The last and largest finite number is 10^604.”
--June 3, 2015

“0 appears to be the last and largest finite number”
--June 9, 2015

“0/0 must be equal to 1.”
-- June 9, 2015

“0 is an infinite irrational number.”
--June 28, 2015

“No negative numbers exist.”
--December 22, 2018

“Rationals are not numbers.”
--May 18, 2019

“The value of sin(45 degrees) = 1.” (It is actually 0.707.)
--May 31, 2019

AP deliberately and repeatedly presented the truth table for OR as the truth table for AND:

“New Logic
AND
T & T = T
T & F = T
F & T = T
F & F = F”
--November 9, 2019

According to AP's “chess board math,” an equilateral triangle is right-triangle.
--December 11, 2019


AP seeks aid of Russian agents to promote failure in schools:

"Please--Asking for help from Russia-- russian robots-- to create a new, true mathematics [sic]"
--November 9, 2017


And if that wasn't weird enough...


AP's sinister Atom God Cult

“The totality, everything that there is [the universe], is only 1 atom of plutonium [Pu]. There is nothing outside or beyond this one atom of plutonium.”
--April 4, 1994

“The Universe itself is one gigantic big atom.”
--November 14, 2019

“Since God-Pu is marching on.
Glory! Glory! Atom Plutonium!
Its truth is marching on.
It has sounded forth the trumpet that shall never call retreat;
It is sifting out the hearts of people before its judgment seat;
Oh, be swift, my soul, to answer it; be jubilant, my feet!
Our God-Pu is marching on.”
--December 15, 2018 (Note: Pu is the atomic symbol for plutonium)

Are you ready, kids???


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]

(correction)

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)

Correction:

=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]]] (max element of s)

Post by Dan Christensen
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]

(Correction)

ALL(s):[Set(s)

& EXIST(a):a in s (s is non-empty)

& ALL(a):[a in s => a<=a] (reflexivity on s)

& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)

& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)

& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)

& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)

& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)

& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)

=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (maximal element on s)


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]

(Correction)

ALL(s):[Set(s)

& EXIST(a):a in s (s is non-empty)

& ALL(a):[a in s => a<=a] (reflexivity on s)

& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)

& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)

& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)

& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)

& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)

& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)

=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

[Mostowski Collapse]

Theorems get more readable if they would use
definitions with self explaining names. You need
to use comments. This is a formalization without

comments, where some definitions are used:

((𝑅 Po 𝐴 ∧ ∀𝑤((𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤) → ...
http://us.metamath.org/mpeuni/zorn2.html

But there is also another version of Zorns
lemma, which is already a step closer to
its application in set theory itself:

∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) →
http://us.metamath.org/mpeuni/zorn.html

Possibly the second version makes use that
any set is partially ordered by set inclusion,
i.e. for any set A, <A,⊊> is a partial order.

Which version do you want to prove?

Post by Dan Christensen
(Correction)
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexivity on s)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)
=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

[Mostowski Collapse]

Corr.: Typo wrong symbol

for any set A, <A,⊆> is a partial order

Post by Mostowski Collapse
Theorems get more readable if they would use
definitions with self explaining names. You need
to use comments. This is a formalization without
((𝑅 Po 𝐴 ∧ ∀𝑤((𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤) → ...
http://us.metamath.org/mpeuni/zorn2.html
But there is also another version of Zorns
lemma, which is already a step closer to
∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) →
http://us.metamath.org/mpeuni/zorn.html
Possibly the second version makes use that
any set is partially ordered by set inclusion,
i.e. for any set A, <A,⊊> is a partial order.
Which version do you want to prove?

Post by Dan Christensen
(Correction)
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexivity on s)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)
=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

[Mostowski Collapse]

Corr.: Typo I didn't copy full condition of zorn2

((𝑅 Po 𝐴 ∧ ∀𝑤((𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤) → ∃𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝑤 (𝑧𝑅𝑥 ∨ 𝑧 = 𝑥))) → ...
http://us.metamath.org/mpeuni/zorn2.html

Also speciality of sets in zorn then, not
only for any set A, <A,⊆> is a partial order,
but also ∪ 𝑧 always exists for z ⊆ A, but not

necessarily inside A. But still the second condition
about boundedness is much shorter formalizable
if you have a definition of ∪:

(∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) → ...
http://us.metamath.org/mpeuni/zorn.html

Arent there definitions in DC Proof? Even not
a definition of like ⊆ ? Why do you need
to painfully write:

ALL(b):[b in a => b in s] (a = subset of s)

Is this a proof system for squirrels?

Post by Mostowski Collapse
Corr.: Typo wrong symbol
for any set A, <A,⊆> is a partial order

Post by Mostowski Collapse
Theorems get more readable if they would use
definitions with self explaining names. You need
to use comments. This is a formalization without
((𝑅 Po 𝐴 ∧ ∀𝑤((𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤) → ...
http://us.metamath.org/mpeuni/zorn2.html
But there is also another version of Zorns
lemma, which is already a step closer to
∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) →
http://us.metamath.org/mpeuni/zorn.html
Possibly the second version makes use that
any set is partially ordered by set inclusion,
i.e. for any set A, <A,⊊> is a partial order.
Which version do you want to prove?

Post by Dan Christensen
(Correction)
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexivity on s)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)
=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

[Dan Christensen]

Post by Mostowski Collapse
Theorems get more readable if they would use
definitions with self explaining names. You need
to use comments. This is a formalization without
((𝑅 Po 𝐴 ∧ ∀𝑤((𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤) → ...
http://us.metamath.org/mpeuni/zorn2.html
But there is also another version of Zorns
lemma, which is already a step closer to
∀𝑧((𝑧 ⊆ 𝐴 ∧ [⊊] Or 𝑧) → ∪ 𝑧 ∈ 𝐴) →
http://us.metamath.org/mpeuni/zorn.html
Possibly the second version makes use that
any set is partially ordered by set inclusion,
i.e. for any set A, <A,⊊> is a partial order.
Which version do you want to prove?

Whichever one is usually used to prove the Well-Ordering Theorem from AC. I've always been a bit sceptical of it and hope to convince myself with DC Proof.


Dan

[Mike Terry]

Post by Dan Christensen
(Correction)
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexivity on s)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (anti-symmetry on s)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transitivity on s)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]] (anti-symmetry on a)
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]] (transitivity on a)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)
=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

Some comments:

1. There are some unnecessary stipulations, which are essentially
harmless:
- s does not need to be assumed non-empty - non-emptiness follows
already from the other stipulations. (But in interesting cases, of
course, s will be non-empty, and ZL is often stated with this stipulation)
- Similarly you don't need to repeat the stipulations for anti-symmetry
and transitivity on the chain a, since these follow already from the
corresponding conditions on s. (Slight inconsistency of approach: there
is no stipulation of reflexivity on s...)

2. You've forgotten to include what is required of the chain a! (It
must have an upper bound in s.)

3. Order of precedence? You have clauses like this:

A & B => C

I take it this means [A & B] => C, not A & [B => C]. (Of course, this
is your system, so you know it, but readers may wonder...)

4. Again with A & B => C, I'd say that most authors phrase this in the
form A => B => C (with => associating from right to left), but your way
is fine. Slight inconsistency: it's best to use one approach
consistently, so if your preference is A & B => C it would be better to
use this also for the maximal element on s.

Regards,
Mike.

[Mike Terry]

Post by Mike Terry

Post by Dan Christensen
(Correction)
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexivity on s)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]]
(anti-symmetry on s)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c =>
a<=c]] (transitivity on s)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (a = subset of s)
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]]
(anti-symmetry on a)
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d =>
b<=d]] (transitivity on a)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]] (connexity on a)
=> EXIST(a):[a in s & ALL(b):[b in s => [a<=b => a=b]]] (maximal element on s)

1. There are some unnecessary stipulations, which are essentially
- s does not need to be assumed non-empty - non-emptiness follows
already from the other stipulations. (But in interesting cases, of
course, s will be non-empty, and ZL is often stated with this stipulation)
- Similarly you don't need to repeat the stipulations for anti-symmetry
and transitivity on the chain a, since these follow already from the
corresponding conditions on s. (Slight inconsistency of approach: there
is no stipulation of reflexivity on s...)
2. You've forgotten to include what is required of the chain a! (It
must have an upper bound in s.)
A & B => C
I take it this means [A & B] => C, not A & [B => C]. (Of course, this
is your system, so you know it, but readers may wonder...)
4. Again with A & B => C, I'd say that most authors phrase this in the
form A => B => C (with => associating from right to left), but your way
is fine. Slight inconsistency: it's best to use one approach
consistently, so if your preference is A & B => C it would be better to
use this also for the maximal element on s.

5. Missing ] at the right hand end of expression :)

Post by Mike Terry
Regards,
Mike.

[Python]

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!)

From what axioms? It has been done in other proof assistants such as Coq
while assuming Axiom of Choice.

[Dan Christensen]

Post by Python

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!)

From what axioms? It has been done in other proof assistants such as Coq
while assuming Axiom of Choice.

From the axioms of set theory (including AC) in my DC Proof program. It will be a good test of my system. I have no intention of publishing it other than here and at my blog.


Dan

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

[Wyatt Adams]

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

Prolog interpreter?

[Dan Christensen]

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.


Dan

[Python]

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)

(what the hell came to your mind when you decide to code
this kind of software in VB???)

[Dan Christensen]

Post by Python

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)
(what the hell came to your mind when you decide to code
this kind of software in VB???)

I knew it.

Dan

[Python]

Post by Dan Christensen

Post by Python

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)
(what the hell came to your mind when you decide to code
this kind of software in VB???)

I knew it.

Hum well...

[James Waldby]

Post by Python

Post by Dan Christensen

Post by Python

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)
(what the hell came to your mind when you decide to code
this kind of software in VB???)

I knew it.

Hum well...

DC started writing his DC Proof and posting about it in sci.math quite
a long time ago. Anyhow, the final release of VB6 was in 1998, and at
the time there were lots of other languages that would have been worse
choices, such as VB1,2,3,4,5.

[Python]

Post by James Waldby

Post by Python

Post by Dan Christensen

Post by Python

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)
(what the hell came to your mind when you decide to code
this kind of software in VB???)

I knew it.

Hum well...

DC started writing his DC Proof and posting about it in sci.math quite
a long time ago. Anyhow, the final release of VB6 was in 1998, and at
the time there were lots of other languages that would have been worse
choices, such as VB1,2,3,4,5.

There was better choices too.

[Mostowski Collapse]

You can cross check whether you have lost
some logical content yourself. Just proof
AC (Axiom of Choice) from Zorns lemma.

AC
|
| proofs only using ZF
|
v
Zorns Lemma
|
| proofs only using ZF
|
v
AC

Are you already done with Zorns Lemma?

Post by Dan Christensen

Post by Python

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Really? Well, may be better that you do not publish the source
code then :-)
(what the hell came to your mind when you decide to code
this kind of software in VB???)

I knew it.
Dan

[Archimedes Plutonium]

POSTED SOME TIME the sci.math in 2019

sex motivation in science Re: curious, just curious-- is there a numbers correlation between percentage of stalkers and homosexuality? Re: Psychology behind the mental disorder of stalking-- kibo Parry Michael Moroney, Dan Christensen, Jan Burse, Jan Bielawski

I am not suggesting that the 12 stalkers are 12 [male --me] homosexuals.

I'm sure they are. That's why they are called /12 Angry Men/!

Well, this explains a lot about many posters in sci.math and sci.physics, for they are not in science for truth but in science to meet and partner up. And explains the loyalty and ferocity of hate posts by those 12, having no truth value. Explains why Franz keeps posting a total fake ellipse, because of his bedwarmer approval.

In another thread I discuss how "money corrupts science" but looking here, I need to consider how sex orientation corrupts the truth of science. So that we must ask-- is black hole acceptance due in large part to homosexual community wanting a black hole agenda. Is the Big Bang theory a homosexual favorite. Is the Appel & Haken in 4 color mapping, the Hales Kepler Packing, the Wiles FLT, all due to homosexual community favoritism, rather than any truth content.

So if Franz can post 100,000 times his fake conic ellipse b.s. all because he wants a bedwarmer, rather than the truth of science. We have to explore how much more of science is a sexual preference rather than reasoned truth.

AP

[Archimedes Plutonium]

Are you ready, kids??? Bend over, er...
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Christensen harps// McGill Univ teaches idiocies//Jack Sankey, Jonathan Sievers, Bradley Siwick, Mark Sutton, Brigitte Vachon,Andreas Warburton, Tracy Webb//ellipse is not conic; real proton= 840MeV not 938; 10 AND 4 = 14 not 10 OR 4 = 14

1.2Christensen harps//Univ Toronto teaches idiocies//Chandler Davis, Spyros Alexakis, Edward Barbeau, Thomas Bloom, Man-Duen Choi, Stephen Cook //ellipse is not conic; real proton= 840MeV not 938; 10 AND 4 = 14 not 10 OR 4 = 14

AP writes: Yes, how does one stop an education parasite like Christensen? Who thinks everyone must learn what "Dan thinks is true", for Dan is a fascist teacher as evidence of his 10 + years of nonstop stalking of AP with his insane 10 OR 4 = 14. Dan should not be in education but in jail or an asylum, in my opinion.

Dan Christensen harps//Univ Western Ontario teaches idiocies// Lisa Thompson, Dan Christensen, Graham Denham, Ajneet Dhillon,Nicole Lemire, Jan Mináč,//ellipse is not conic; real proton= 840MeV not 938; 10 AND 4 = 14 not 10 OR 4 = 14

Dan Christensen wrote:
WARNING TO STUDENTS: Don't become a victim
On Saturday, June 1

AP writes: yes a victim of Dan's 10 OR 4 = 14 with 10 AND 4 = 6

AP writes: Is the reason Canada has not yet confirmed real proton is 840MeV not 938, because its scientists behave like Christensen-- cesspool mind of hatred with daily hate sheets on people rather than spend their daily activity on uncovering the true proton is 840MeV stuck with the real electron as muon doing the Faraday law to create Dirac magnetic monopoles.


       o-:^>___?
       `~~c--^c'
Navy dog says: yea yea

Remember the time the Dan Christensen could not tell the difference between distinct and nondistinct.

PAGE58, 8-3, True Geometry / correcting axioms, 1by1 tool, angles of logarithmic spiral, conic sections unified regular polyhedra, Leaf-Triangle, Unit Basis Vector
The axioms that are in need of fixing is the axiom that between any two points lies a third new point.

The should be "between and any two DISTINCT points."

What a monsterous fool you are

OMG. You are serious. Stupid and proud of it.

And yet Mr Plutonium is right.  Two points are distinct (else they would
be one) and it is not necessary to say so.

McGill University Physics department

Kartiek Agarwal, Robert Brandenberger, Thomas Brunner, Fritz Buchinger, Simon Caron-Huot, Cynthia Chiang, Lily Childress, Jim Cline, Bill Coish, David Cooke, Francois Corriveau, Nicolas Cowan, Andrew Cumming, Keshav Dasgupta, Matt Dobbs, Paul Francois, Charles Gale, Guillaume Gervais, Martin Grant, Peter Grutter, Hong Guo, Daryl Haggard, David Hanna, Sarah Harrison, Michael Hilke, Sangyong Jeon, Victoria M. Kaspi, Eve Lee, Sabrina Leslie, Adrian Liu, Shaun Lovejoy, Alexander Maloney, Tami Pereg-Barnea, Nikolas Provatas, Kenneth Ragan, Walter Reisner, Steven Robertson, Robert E. Rutledge, Dominic H. Ryan, Jack Sankey, Jonathan Sievers, Bradley Siwick, Mark Sutton, Brigitte Vachon, Andreas Warburton, Tracy Webb, Paul Wiseman


Univ of Victoria physics dept
Justin Albert, Arif Babul, Devika Chithrani, Byoung-Chul Choi, Rogerio de Sousa, Ruobing Dong, Sara L. Ellison, Falk Herwig, Dean Karlen, Richard K. Keeler, Jody Klymak, Pavel Kovtun, Robert V. Kowalewski, Mark Laidlaw, Michel Lefebvre, Travis Martin, Julio Navarro, Maxim Pospelov, Adam Ritz, J.Michael Roney, Geoffrey M. Steeves, Kim Venn, Jon Willis


Univ Western Ontario math dept
Janusz Adamus, Tatyana  Barron,   Dan Christensen, Graham Denham, Ajneet Dhillon, Matthias  Franz, John Jardine, Massoud Khalkhali, Nicole Lemire, Jan Mináč, Victoria Olds, Martin Pinsonnault, Lex Renner, David Riley, Rasul Shafikov, Gordon Sinnamon

Chancellor Linda Hasenfratz
President Alan Shepard
Amit Chakma (chem engr)

Univ. Western Ontario physics dept
Pauline Barmby, Shantanu Basu, Peter Brown, Alex Buchel, Jan Cami, Margret Campbell-Brown, Blaine Chronik, Robert Cockcroft, John R. de Bruyn, Colin Denniston, Giovanni Fanchini, Sarah Gallagher, Lyudmila Goncharova, Wayne Hocking, Martin Houde, Jeffrey L. Hutter, Carol Jones, Stan Metchev, Silvia Mittler, Els Peeters, Robert Sica, Aaron Sigut, Peter Simpson, Mahi Singh, Paul Wiegert, Eugene Wong, Martin Zinke-Allmang


Univ Toronto, physics, Gordon F. West, Michael B. Walker, Henry M. Van Driel, David J. Rowe, John W. Moffat, John F. Martin, Robert K. Logan, Albert E. Litherland, Roland List, Philipp Kronberg, James King, Anthony W. Key, Bob Holdom, Ron M. Farquhar, R. Nigel Edwards, David J. Dunlop, James Drummond, Tom E. Drake, R.Fraser Code, Richard C. Bailey, Robin Armstrong

Univ Toronto math dept
Mustafa Akcoglu, Spyros Alexakis, Edward Barbeau, Thomas Bloom, Man-Duen Choi, Stephen Cook, Chandler Davis, Nicholas Derzko, Eric Ellers, Ilya Gekhtman, Ian Graham, Steve Halpern, Wahidul Haque, Abe Igelfeld, Velimir Jurdjevic, Ivan Kupka, Anthony Lam, Michael Lorimer, James McCool, Eric Mendelsohn, Kunio Murasugi, Jeremy Quastel, Peter Rosenthal, Paul Selick, Dipak Sen, Rick Sharpe, Stuart Smith, Frank Tall, Steve Tanny

can't figure out prime numbers (like so many things), so he calls them "fake." What an idiot!

Christensen says Lisa Thompson,Univ Toronto & Western Ontario, David J. Dunlop, James Drummond, Tom E. Drake, R.Fraser Code, Richard C. Bailey-- cannot confirmed real proton = 840MeV, real electron is the muon and .5MeV was Dirac monopole, can't figure


AP writes: Yes we are fed up with the likes of the failure of Dan Christensen who preaches 10 OR 4 = 14 with 10 AND 4 = 6; never has a geometry proof of Fundamental Theorem of Calculus, and preaches the ellipse is a conic when it never was.

1.0-Set theory completely thrown out of science and math

WARNING TO STUDENTS: Don't be a victim of AP's fake math and science

I like to laugh at people in wheelchairs and people with white sticks.

                              ..
            .- " `-.   ,..-'''  ```....'`-..
           ,      . `.'            '        `.
         .'   .' `    `           '   `..     ;
         .   ;  .'                     . `.    ;
         ;   . '                       `.  .   '
          . '                            ` `.  |
        . '.                                  '
       .          0              0            ' `.
      '                                          `
     ;                                            `
    .'                                             `
    ;                      U                        `
    ;    ';                                         `
    :   | ;..                                 :`     `
    :    `;. ```.                           .-; |    '
    '.      `    ``..,                   .'   :'    '
     ;       `        ;'..          ..-''    '     '  I am Christensen,I am such a stupid insane imp of math and logic that I thought a vertex has a derivative, that distinct means not-distinct, and that 10 OR 4 = 14 with 10 AND 4 = 6, when a 8 year old knows 10 AND 4= 14 . And I love spam reading of vvgra and tomato hello, and I am a failure of academics and so I spend most days making out hate-lists of people who actually succeed in science for my pea sized brain is envious of those who succeed in science yet I failed in science.
      `       `        ;  ````'''""'  ;      '    '
       `       `        ;            ;      '    '
        `       `        ;          ;      '    '
         `       `.       ````''''''      '    '
           `       .                     '    '
         /  `       `.                  '    '        .
        /     `       ..            ..'    .'"""""...'
       /   .`   `       ``........-'     .'` .....'''
      / .'' ;     `                    .'   `
  ...'.'    ;    .' `                .'      `
   ""      .'  .' |    `           .; \       `
           ; .'   |      `. . . . ' .  \       `
           :'     |     '   `       ,   `.     `
                  |    '     `      '     `.    `
                  `   '       `     ;       `.  |
                  `.'          `    ;         `-'
                                `...'


Christensen asks Univ Western Ontario Drs  Peter Brown, Alex Buchel, Jan Cami which is AP's 2nd greatest theory- Sun and Stars are powered by Faraday Law of atoms, or, AP theory that Real Proton = 840 MeV with electron= muon and .5MeV was Dirac magnetic monopole  

Canadian Educ Ministers-- endorsing stalking hypocrites like Dan Christensen with his insane 2 OR 10 = 12 when even a Canadian 8 year old knows 2 AND 10 = 12. Endorsing the "perpetual stalking by Dan Christensen"

Lisa Thompson, Sebastien Proulx, Jordan Brown, David Eggen, Gordon Wyant, Zach Churchill, Ian Wishart, Rob Fleming.


David Eggen, Gordon Wyant, Zach Churchill,UWO's,Matthias  Franz,John Jardine,Massoud Khalkhali,Nicole Lemire// Are you as ignorant and a education parasite as Christensen on the ELLIPSE is never a conic??

Definition: education parasite: a person or a group of people that values money or convenience ahead of the Truth. They never want to fix errors but teach errors forever because it takes time and money out of them to teach the truth.



   /\-------/\
   \::O:::O::/
  (::_  ^  _::)
   \_`-----'_/
You mean the classroom is the world, not just my cubbyhole in Canada.
And, even though you-- professors of physics, want to remain stupid in not knowing what is really the electron in atoms has to be the muon at 105MeV and proton at 840MeV with Dirac's magnetic monopole being .5MeV, your students deserve better. Or math professors remaining stupid on ellipse is never a conic, 3 OR 2 = 5 is bad failed logic and Trig is based on semicircle wave, not sinusoid.

The world no longer needs physics professors who cannot understand Angular Momentum and that the Chemical bond cannot exist with proton = 938MeV, electron= .5MeV.

Yes, there, what did they say-- the power of Sun and stars is not really fusion but is the Faraday Law inside of atoms creating monopoles and turning Space into energy that fuels the Sun and stars. My rough estimate is that fusion only supplies 10% or less of Sun and stars.

But of course, I could not have discovered the true starpower when under the idiotic idea that the electron was a mere .5MeV when it truly is 105 MeV.

What answer did they give?

And what is this connection of Dan Christensen with John Baez if such. Are they aiding and abetting stalking?? Running some computer program of stalking in sci.math & sci.physics, if such.

UC Riverside Math Dept, provost: Cynthia Larive- chemist,
Mark Alber, John Baez, Mei-Chu Chang, Vyjayanthi Chari, Kevin Costello, Po-Ning Chen, Wee Liang Gan, Gerhard Gierz, Jacob Greenstein, Jose Gonzalez, Zhuang-dan Guan, Jim  Kelliher, Sara Lapan, Michel Lapidus, Carl Mautner, Amir  Moradifam, Yat Sun Poon, Ziv Ran, David Rush, Reinhard Schultz, Stefano Vidussi, David Weisbart, Fred Wilhelm, Bun Wong, Yulong Xing, Feng Xu, Qi Zhang




   /\-------/\
   \::O:::O::/
  (::_  ^  _::)
   \_`-----'_/
You mean the classroom is the world, not just my cubbyhole in Canada?

Yes, what did they say-- the power of Sun and stars is not really fusion but is the Faraday Law inside of atoms creating monopoles and turning Space into energy that fuels the Sun and stars. My rough estimate is that fusion only supplies 10% or less of Sun and stars.

But of course, I could not have discovered the true starpower when under the silly idea that the electron was a mere .5MeV when it truly is 105 MeV.

In that manner,  physics departments are racist physicists for the knowledge that Real Electron = 105MeV, Real Proton = 840 MeV, and the .5MeV was Dirac's Magnetic Monopole is going on 2 years now in the public eye starting 2017, yet none of these physicists (these poor physicists lacking understanding of angular momentum has raised a single peep). The reason they keep their mouths shut, is because they are so poor in physics, they do not want to be embarrassed. These gentlemen and ladies are not physicists, for a real physicist would debate the issue, not hide from the issue. And real physicist would not discount a discovery because of the person-- Archimedes Plutonium who discovered it.

Cynthia Larive,Mark Alber,John Baez, UC-Riverside vs. Matthias Franz,Nicole Lemire,UWO// Dan asks for sine of 45 degrees in your goofy math--when you still teach the ellipse is a conic when it never was-- are you all education parasites?(see proof)

Did you ever figure out the sine of 45 degrees in your new trig system,

Cynthia Larive,Mark Alber,John Baez, UC-Riverside vs. Matthias Franz,Nicole Lemire,UWO// Dan asks for sine of 45 degrees in you goofy math-- when you still teach the ellipse is a conic when it never was-- are you all education parasites? (see proof below)

Newsgroups: sci.physics
Date: Sun, 12 Mar 2017 00:28:31 -0800 (PST)
In-Reply-To: <421c6f56-7355-4ec6-9747-***@googlegroups.com>
Complaints-To: ***@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=192.208.232.34;
 posting-account=jPnQ2goAAAA461y3QD0lbyw0oKeThma1
NNTP-Posting-Host: 192.208.232.34
References: <0f307785-464a-4e59-b400-***@googlegroups.com>
 <a06f5f30-857e-4c33-9094-***@googlegroups.com> <afe56d2e-3fca-4c76-81da-***@googlegroups.com>
 <421c6f56-7355-4ec6-9747-***@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <69d8bde6-bcb6-472f-9765-***@googlegroups.com>
Subject: asshole
From: noTthaTguY <***@gmail.com>
Injection-Date: Sun, 12 Mar 2017 08:28:33 +0000

ellipses are ovals, but not all ovals are elipses, of course;
just grab a dictionary, asshole

Robin Armstrong,Mustafa Akcoglu,Spyros Alexakis,Univ Toronto asked by UWO Dan Christensen asks for the sine of 45 degrees in their goofy trig system, never realizing the sine function is actually a semicircle wave?


Robin Armstrong,Mustafa Akcoglu,Spyros Alexakis,Univ Toronto asked by UWO Dan Christensen asks for the sine of 45 degrees in their goofy trig system, never realizing the sine function is actually a semicircle wave?

STILL cannot even give us the sine of 45 degrees in his goofy trig system. Again, he just runs away and hides, desperately trying to change the subject.
Dan

 

David Eggen, Gordon Wyant, Zach Churchill,UWO's,Matthias  Franz,John Jardine,Massoud Khalkhali,Nicole Lemire// Are you as ignorant and a education parasite as Christensen on the ELLIPSE is never a conic??

Definition: education parasite: a person or a group of people that values money or convenience ahead of the Truth. They never want to fix errors but teach errors forever because it takes time and money out of them to teach the truth.



   /\-------/\
   \::O:::O::/
  (::_  ^  _::)
   \_`-----'_/
You mean the classroom is the world, not just my cubbyhole in Canada.
And, even though you-- professors of physics, want to remain stupid in not knowing what is really the electron in atoms has to be the muon at 105MeV and proton at 840MeV with Dirac's magnetic monopole being .5MeV, your students deserve better. Or math professors remaining stupid on ellipse is never a conic, 3 OR 2 = 5 is bad failed logic and Trig is based on semicircle wave, not sinusoid.

The world no longer needs physics professors who cannot understand Angular Momentum and that the Chemical bond cannot exist with proton = 938MeV, electron= .5MeV.

And, even though you-- professors of physics/math, want to remain silent and stupid in Real Electron = muon, and true real Calculus with a geometry proof of Fundamental Theorem of Calculus, your students deserve better.

Yes, there, what did they say-- the power of Sun and stars is not really fusion but is the Faraday Law inside of atoms creating monopoles and turning Space into energy that fuels the Sun and stars. My rough estimate is that fusion only supplies 10% or less of Sun and stars.

But of course, I could not have discovered the true starpower when under the idiotic idea that the electron was a mere .5MeV when it truly is 105 MeV.

What answer did they give?

Christensen asks Univ Western Ontario Drs  Peter Brown, Alex Buchel, Jan Cami which is AP's 2nd greatest theory- Sun and Stars are powered by Faraday Law of atoms, or, AP theory that Real Proton = 840 MeV with electron= muon and .5MeV was Dirac magnetic monopole  
Canadian Educ Ministers-- endorsing stalking hypocrites like Dan Christensen with his insane 2 OR 10 = 12 when even a Canadian 8 year old knows 2 AND 10 = 12. Endorsing the "perpetual stalking by Dan Christensen"

Sebastien Proulx, Jordan Brown, David Eggen, Gordon Wyant, Zach Churchill, Ian Wishart, Rob Fleming, Justin Trudeau


Alan Richard Bundy, Gregory Chaitin,Jack Copeland, John Corcoran, are you a moron of logic, like Christensen in Logic with 3 OR 2 = 5 with 3 AND 2 = 1 embracing the contradiction of Either..Or..Or..Both


Alan Richard Bundy, Gregory Chaitin,Jack Copeland, John Corcoran, are you a moron of logic, like Christensen in Logic with 3 OR 2 = 5 with 3 AND 2 = 1 embracing the contradiction of Either..Or..Or..Both

Were you ever able to obtain a value for the sine of 45 degrees in your goofy trig system,

AP writes: Forget about trig for the moment for Alan Richard Bundy, Gregory Chaitin,Jack Copeland, John Corcoran have far larger problems.

Definition: education parasite: a person or a group of people that values money or convenience ahead of the Truth. They never want to fix errors but teach errors forever because it takes time and money out of them to fix errors and teach the truth.
 

Jean-Yves Beziau,Andrea Bonomi,Nicolas Bourbaki (a group of logic fumblers) are you? an education parasite on Logic as is Christensen with 3 OR 2= 5 while their 3 AND 2 = 1, embracing the contradiction Either..Or..Or..Both

Peter Bruce Andrews, Lennart Aqvist, Henk Barendregt, John Lane Bell, are you an education parasite on Logic as is Christensen with 3 OR 2= 5 while their 3 AND 2 = 1, embracing the contradiction Either..Or..Or..Both

Dan
Download my DC Proof 2.0,,,,
Visit my Math Blog,,,

(be foolish and download that worthless moneygrub parasite of Logic-- Christensen)

Scientists that are just memorization not masters Re: Analysis of failures..Logic with failures of Physics// one thinks 3 OR 2 =5 with 3 AND 2 = 1 while the other thinks proton to electron is 938MeV vs .5MeV when truly it is 840MeV to 105MeV

Dan Christensen (the stalking insane Canadian of 6 years) wrote on 20Dec2018
8:19 AM (11 hours ago)

WARNING TO PARENTS
Archie Pu's fake logic

A    B    A & B
T    T        T
T    F        T
F    T        T
F    F        F
A    B    A & B
T    T        T
T    F        F
F    T        F
F    F        F

A    B    A OR B
T    T        T
T    F        T
F    T        T
F    F        F


Partial List of the World's Crackpot Logicians-- should be in a college Abnormal-Psychology department, not Logic//


Peter Bruce Andrews, Lennart Aqvist, Henk Barendregt, John Lane Bell, Nuel Belnap,
Paul Benacerraf, Jean Paul Van Bendegem, Johan van Benthem, Jean-Yves Beziau,
Andrea Bonomi, Nicolas Bourbaki (a group of logic fumblers), Alan Richard Bundy, Gregory Chaitin,
Jack Copeland, John Corcoran, Dirk van Dalen, Martin Davis, Michael A.E. Dummett, John Etchemendy, Hartry Field, Kit Fine, Melvin Fitting, Matthew Foreman, Michael Fourman,
Harvey Friedman, Dov Gabbay, L.T.F. Gamut (group of logic fumblers), Sol Garfunkel, Jean-Yves Girard, Siegfried Gottwald, Jeroen Groenendijk, Susan Haack, Leo Harrington, William Alvin Howard,
Ronald Jensen, Dick de Jongh, David Kaplan, Alexander S. Kechris, Howard Jerome Keisler,
Robert Kowalski, Georg Kreisel, Saul Kripke, Kenneth Kunen, Karel Lambert, Penelope Maddy,
David Makinson, Isaac Malitz, Gary R. Mar, Donald A. Martin, Per Martin-Lof,Yiannis N. Moschovakis, Jeff Paris, Charles Parsons, Solomon Passy, Lorenzo Pena, Dag Prawitz,
Graham Priest, Michael O. Rabin, Gerald Sacks, Dana Scott, Stewart Shapiro, Theodore Slaman,
Robert M. Solovay, John R. Steel, Martin Stokhof, Anne Sjerp Troelstra, Alasdair Urquhart,
Moshe Y. Vardi, W. Hugh Woodin, John Woods

Now I should include the authors of Logic textbooks for they, more than most, perpetuate and crank the error filled logic, the Horrible Error of 4 OR 3 = 7 with 4 AND 3 = 1, that is forced down the throats of young students, making them cripples of ever thinking straight and clearly.

Many of these authors have passed away but their error filled books are a scourge to modern education

George Boole, William Jevons, Bertrand Russell, Kurt Godel, Rudolf Carnap,
Ludwig Wittgenstein, Willard Quine, Alfred North Whitehead, Irving Copi, Michael Withey,
Patrick Hurley, Harry J Gensler, David Kelley, Jesse Bollinger, Theodore Sider,  
David Barker-Plummer, I. C. Robledo, John Nolt, Peter Smith, Stan Baronett, Jim Holt,
Virginia Klenk, David Agler, Susanne K. Langer, Gary M. Hardegree, Raymond M. Smullyan,
John Venn, William Gustason, Richmond H. Thomason,  

All of them are clowns of logic, although they have interest in logic, none are past a baby stage understanding of what Logic is. They are all worse than the fool George Boole. All of them are a disgrace to the subject we call Logic. All of them are in the same boat as George Boole-- catching pneumonia and then having his wife douse him in bed with cold freezing water and taking cold showers-- thinking that combatting pneumonia is done by getting colder.

All of the above listed should never be allowed to teach their nonsense and pollute the minds of youngsters with their crazy 9 OR 5 = 14 with 9 AND 5 = 4, all because a crazy Boole with Jevons in the 1800s thought that OR was add and AND was subtract. All because a true logician has more than a microgram brain of Logic in his head, and realizes that if you had a string of statements, say 10 statements and if just one single statement of those ten is true, makes the entire set of 10 to be true also, regardless of the truth value of the other 9 statements. Said in a different manner, if you have a truth of a single statement, and, no matter how you surround that single statement with 9 other statements, regardless of their truth value, because of the truth of the one statement makes the combined all 10 statements have a true value.

The stupid microgram brain of Boole and Jevons in the subject of Logic (witness their history with pneumonia) is not a Logic at all, for it leads to the incredibly stupid formulation that 3 AND 2 = 1 with 3 OR 2 = 5. Yes, those two logical idiots Boole and Jevons and every idiot of Logic since those two, have thought the truth table of AND was TFFF, when according to a real true logical person-- you need just 1 true statement to make a compound statements as a whole be true. So the true true truth table of AND was TTTF. And this makes sense in the above idiots of Logic with their OR, so confused were those idiots that they combined a "or" with an "and" and generated a "inclusive or" of TTTF. I mean what clowns are these? Who think that OR has to be compounded or a composite of "and", with "or" forming the idiot idea of an "inclusive or" and, not even realizing that you no longer have a primitive-connector. The true truth table of OR is exclusive and is FTTF, which is subtraction in mathematics.


Inclusive OR, INCLUSIVE OR, is the invention of an idiot of logic, pure slab of bonehead worthless bonehead of Logic, for the "inclusive or" is a village idiot mind that stacks together the OR and the AND all into one idiotic product of Either ,,Or,, Or Both. Not an accident waiting to happen in Logic, a multiple chain collision on the expressway is the Either Or Or Both. It is not a primitive logical Connector that the 4 primitive logic Connectors need to be, no, the Either Or Or Both is already a fool's built compound connector pretending to be primitive connector. A village idiot of the 1800s like George Boole and his compatriot Jevons would not have enough of a logical mind to see that Either Or Or Both is a compound piece of worthless nonsense. Even a 8 year old can see that Either Or Or Both is a compounded piece of crap and has no business of being in Logic primitive connectors.

To be in Logic, you need a Logical Mind to even do logic, and to come up with a SELF CONTRADICTION in terms like it is updown or it is overeasy-hard, is the same as Inclusive-Or, a term and idea that is a self-contradiction. Logic is about staying away from contradiction. And here, starting with Boole and Jevons, they built their logic on a Contradiction of the inclusive-or. It would be like at the Olympics in the 100 meter dash, at the sound of the gun, a runner, instead of going forwards, goes backwards in running step in the dash, not to the finish line but to oblivion running backwards.


So, please stop torturing the brains and minds of our young students just because you are a clown of microgram brain of logic. And throw out all the OLD LOGIC textbooks for they are not learning or teaching but brainwashing by polluting moneygrubs, more concerned over money flow than what is the truth of logic.

#1 first comes Logic-- think straight and clear which many math professors are deaf dumb and blind to

My corrections of Old Logic have a history that dates before 1993, sometime around 1991, I realized the Euclid proof of infinitude of primes was illogical, sadly sadly wrong, in that the newly formed number by "multiply the lot and add 1" was necessarily a new prime in the indirect proof method. So that my history of fixing Old Logic starts in 1991, but comes to a synthesis of correcting all four of the connectors of Equal/not, And, Or, If->Then, by 2015.

History of AP Logic starts with 1991 and culminates with New Logic that replaces Old Logic by 2015. Old Logic is like comparing a flat earth theory to a true round earth theory.

Before you do Mathematics, you need to be able to think correctly, straight and clear. Unfortunately schools across the world do not teach proper true Logic. They teach a mish mash gaggle of error filled garbage and call it Logic.


The 4 connectors of Logic are:

1) Equal (equivalence) plus Not (negation) where the two are combined as one
2) And (conjunction)
3) Or (exclusive or) (disjunction)
4) Implication

New Logic

EQUAL/NOT table:
T  = T  = T
T  = not F  = T
F  = not T  = T
F =  F   = T

Equality must start or begin logic because in the other connectors, we
cannot say a result equals something if we do not have equality built
already. Now to build equality, it is unary in that T=T and F =F. So
we need another unary connector to make equality a binary. Negation is
that other connector and when we combine the two we have the above
table.

Equality combined with Negation allows us to proceed to build the
other three logic connectors.

Now, unfortunately, Logic must start with equality allied with
negation and in math what this connector as binary connector ends up
being-- is multiplication for math. One would think that the first
connector of Logic that must be covered is the connector that ends up
being addition of math, not multiplication. But maybe we can find a
philosophy-logic answer as to why Logic starts with equal/not and is
multiplication rather than addition. That explanation is of course the Space in which the Logic operators govern, and the full space is area, so that is multiplication. And we see that in a geometry diagram

T    T

T    T where all four small squares are T valued making a 4 square

While addition is and with a Space like this

T    T

T    F and we have just 3 of the 4 smaller squares covered by addition.

Here you we have one truth table equal/not whose endresult is 4 trues and now we move on to AND as addition.

New Logic
AND
T &  T  = T
T & F  = T
F &  T  = T
F  & F   = F

AND is ADD in New Logic, and that makes a whole lot of common sense.
AND feels like addition, the joining of parts. And the truth table for
AND should be such that if given one true statement in a series of
statements then the entire string of statements is true. So if I had P
and Q and S and R, I need only one of those to be true to make the
string true P & Q & S & R = True if just one statement is true.

The truth table of AND results in 3 trues and 1 false.

New Logic
OR(exclusive)
T or  T  = F
T or F  = T
F or  T  = T
F  or F   = F

OR is seen as a choice, a pick and choose. So if I had T or T, there
is no choice and so it is False. If I had T or F there is a choice and
so it is true. Again the same for F or T, but when I have F or F,
there is no choice and so it is false. OR in mathematics, because we
pick and discard what is not chosen, that OR is seen as subtraction.

OR is a truth table whose endresult is 2 trues, 2 falses.

New Logic
IMPLIES (Material Conditional)
IF/THEN
MOVES INTO
T ->  T  = T
T ->  F  = F
F ->  T  = U probability outcome
F ->  F   = U probability outcome

A truth table that has a variable which is neither T or F, but U for
unknown or a probability outcome. We need this U so that we can do
math where 0 divided into something is not defined.

Now notice there are four truth tables where the endresult is 4 trues,
3 trues with 1 false, 2 trues with 2 falses and finally a truth table
with a different variable other than T or F, with variable U. This is
important in New Logic that the four primitive connectors, by
primitive I mean they are independent of one another so that one
cannot be derived by the other three. The four are axioms,
independent. And the way you can spot that they are independent is
that if you reverse their values so that 4 trues become 4 falses. For
AND, reversal would be FFFT instead of TTTF. For OR, a reversal would
be TFFT instead of FTTF.

To be independent and not derivable by the other three axioms you need
a condition of this:

One Table be 4 of the same
One Table be 3 of the same
One Table be 2 of the same
And to get division by 0 in mathematics, one table with a unknown variable.

So, how did Old Logic get it all so wrong so bad? I think the problem
was that in the 1800s when Logic was being discovered, is that the
best minds of the time were involved in physics, chemistry, biology
and looked upon philosophy and logic as second rate and that second
rate minds would propose Old Logic. This history would be from Boole
1854 The Laws of Thought, and Jevons textbook of Elementary Lessons on
Logic, 1870. Boole started the Old Logic with the help of Jevons and
fostered the wrong muddleheaded idea that OR was ADD, when it truly is
AND.

Now the way people actually live, is an indicator of how well they
thought and how well any of their ideas should be taken seriously. In
the case of Boole, he went to class in a downpour rain, why without a
raincoat? And reaching class, instead of changing into dry warm
clothes, stood for hours in front of students, sopping wet and
shivering. Of course he caught pneumonia, but instead of being
sensible, common sense that even a fly would have, he insisted his
wife give him cold showers and make the bed all wet and freezing. Of
course, he would die from this. Now, does anyone today, think that a
mind like that has anything to offer Logic or mathematics, is as crazy
as what Boole was.

But once you have textbooks about Logic, it is difficult to correct a
mistake because of the money making social network wants to make more
money, not go around fixing mistakes. So this nightmarish mistakes of
the truth tables was not seen by Frege, by Russell, by Whitehead, by
Carnap, by Godel, and by 1908 the symbols and terminology of the Old
Logic truth tables were so deeply rooted into Logic, that only a
Logical minded person could ever rescue Logic.

1.1 The "and" truth table should be TTTF not what Boole thought TFFF.
Only an utter gutter mind of logic would think that in a series of
statements, that AND is true when all statements are true, but to the
wise person-- he realizes that if just one statement is true, the
entire series is true, where we toss aside all the irrelevant and
false statements --(much what life itself is-- we pick out the true
ones and ignore all the false ones). In fact, in a proof in mathematics, the proof can be full of false and nonsense statements, so long as the proof itself is there and be seen as overall True. For example the proof of SAS in geometry, side angle side, can be packed with false statements and irrelevant statements and still be true.
1.2 The error of "if-then" truth table should be TFUU, not that of TFTT
1.3 The error of "not" and "equal", neither unary, but should be binary
1.4 The error that Reductio Ad Absurdum is a proof method, when it is
merely probability-truth, not guaranteed
1.5 The error, the "or" connector is truth table FTTF, never that of TTTF, for the idea of an inclusive "or", --- either A or B or both, is a self contradiction. And funny, how the fathers of Logic-- Boole and Jevons had a connector that was self contradictory, as if the fathers of logic had no logical mind to be doing logic in the first place.

1.6 So that begs the question, what in mathematics has a truth table of TFFF. Well the simple answer is that it is a reverse of TTTF which is AND, and so the former can be got by that of a NOT function on AND. But in isolation, what is a table of TFFF in mathematics? My guess is it is Absolute Value, a form of Absolute Value in mathematics, but that is only a guess. In 2016 I gave a half hearted argument that TFFF was absolute value.

[Chris M. Thomasson]

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Holy shi%. I used that way back in the day. Remember using it with some
Access databases for a reporting system.

[Chris M. Thomasson]

Post by Chris M. Thomasson

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Holy shi%. I used that way back in the day. Remember using it with some
Access databases for a reporting system.

Damn. I still have my service pack 3 CD.

[Will Houser]

Post by Chris M. Thomasson

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Holy shi%. I used that way back in the day. Remember using it with some
Access databases for a reporting system.

I used it a few times, and felt insulted. Intended by microsoft, I guess,
to be what android sdk is for google now. But taking money for it, not
good. They learned a lesson.

[Chris M. Thomasson]

Post by Will Houser

Post by Chris M. Thomasson

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Holy shi%. I used that way back in the day. Remember using it with some
Access databases for a reporting system.

I used it a few times, and felt insulted.

;^)

I basically used it for a quick GUI for a database. It intermingled with
ms word as well.


Intended by microsoft, I guess,

Post by Will Houser
to be what android sdk is for google now. But taking money for it, not
good. They learned a lesson.

Check out Q#:

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

;^) I actually have this up and running.

[Python]

Chris M. Thomasson wrote:
...

Post by Chris M. Thomasson
https://en.wikipedia.org/wiki/Q_Sharp
;^) I actually have this up and running.

Please do not use a Microsoft language to do Quantum
Computing, it's likely to crash the whole Universe.

[Chris M. Thomasson]

Post by Python
...

Post by Chris M. Thomasson
https://en.wikipedia.org/wiki/Q_Sharp
;^) I actually have this up and running.

Please do not use a Microsoft language to do Quantum
Computing, it's likely to crash the whole Universe.

LOL! Damn, you are probably right. I installed it out of sheer
curiosity. Fwiw, my main languages of choice are C and C++. However, I
do some Python and JavaScript as well. Check out the example code in
section 5 Appendix:

http://funwithfractals.atspace.cc/ct_cipher
(python 3)

Have a crude C version of this here:

https://groups.google.com/d/topic/comp.lang.c/a53VxN8cwkY/discussion

https://pastebin.com/raw/feUnA3kP
(C version)

[Will Houser]

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Then not even of an introductory new-beginner level. Tell me why should I
waste my time?

[Dan Christensen]

Post by Will Houser

Post by Dan Christensen

Post by Wyatt Adams

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

Prolog interpreter?

No. It is written in Visual Basic 6.

Then not even of an introductory new-beginner level.

Huh??? DC Proof 2.0 is a program written in the VB6 language. (The original version in VBDOS.). The user does not need to use VB6 or any other programming language.

The tutorial starts by proving with P & Q => Q & P.

1 P & Q
Premise

2 P
Split, 1

3 Q
Split, 1

4 Q & P
Join, 3, 2

5 P & Q => Q & P
Conclusion, 1

To begin, the user clicks the Premise button on the main screen and keys in "P & Q" to obtain line 1. From here on, it's all point and click. No more typing.

To obtain lines 2 and 3, the user clicks the Split button and points to line 1.

To obtain line 4, the user clicks the Join button, then points to line 3, then line 2.

To obtain line 5, the user simply clicks the Conclusion button.


Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com <--- See screen shots
Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

3rd draft

Notation:

Set(x) = x is a set
Sub(x,y) = x is a subset of y
x in y = x is an element of y
'|' = OR-operator


Zorn's Lemma?

ALL(a):[Set(a)
& EXIST(b):b in a
& PartialOrder(a)
& ALL(b):[Sub(b,a) => [TotalOrder(b) => EXIST(c):[c in a & UpperBound(b,c)]]]

=> EXIST(b):[b in a & Maximal(a,b)]]



Define: Sub(x,y) (x is a subset of y)

1 ALL(a):ALL(b):[Sub(a,b)
<=> ALL(c):[c in a => c in b]]
Axiom

Define: PartialOrder(x) (x has a partial ordering <=)

2 ALL(a):[PartialOrder(a)
<=> ALL(b):[b in a => b<=b]
& ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]]
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]]]
Axiom

Define: TotalOrder(x) (x has a total ordering <=)

3 ALL(a):[TotalOrder(a)
<=> ALL(b):ALL(c):[b in a & c in a => [b<=c & c<=b => b=c]]
& ALL(b):ALL(c):ALL(d):[b in a & c in a & d in a => [b<=c & c<=d => b<=d]]
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b]]
Axiom

Define: Upperbound(x,y) (the upper bound of set x under <= is y)

4 ALL(a):ALL(b):[UpperBound(a,b)
<=> ALL(c):[c in a => c<=b]]
Axiom

Define: Maximal(x,y) (y is a maximal element of set x under <=)

5 ALL(a):ALL(b):[Maximal(a,b)
<=> ALL(c):[c in a => [b<=c => b=c]]]
Axiom

[Archimedes Plutonium]

Post by Dan Christensen
3rd draft

Dan, did you come out of the woodwork in High School biology class or math class? Kibo Parry wants to know.

Re: 2-Dan Christensen and Jan Burse, the arsewipes of Logic with their 2 OR 3 = 5 and their mind numbing belief a ellipse is a conic section when it never was-- it was a cylinder section
8 posts by 5 authors

11:47 AM (5 hours ago)

Me On Monday, May 4, 2020 at 6:42:11 PM UTC+2, Archimedes Plutonium wrote: > an ellipse is a conic section Right. Want to see my proof again? Here's an alternative proof based on Dandelin's spheres: http://www.nabla.hr/CO-ConicsProperties2.htm#Da

This message has been deleted.

11:57 AM (5 hours ago)

Dan Christensen Archie Pu is not interested in proofs. He only cares about promoting failure in schools and recruiting the dropouts to his Atom God Cult of Failure. Think I'm making this up? IN HIS OWN WORDS: AP's fake math that can only be designed to promote

12:10 PM (5 hours ago)

me 2-Dan Christensen and Jan Burse, the arsewipes of Logic with their 2 OR 3 = 5 and their mind numbing belief a ellipse is a conic section when it never was-- it was a cylinder section 3 posts by 3 authors me (Archimedes Plutonium change)

12:14 PM (5 hours ago)

Me your hat in science. I like your sense of humor. :-) Actually, you can't compare *me* with JG!

12:16 PM (5 hours ago)

Python section Did it come in your (aheum) mind, that it may be both?

12:47 PM (4 hours ago)

me Did it ever occur to you that you being gay, has a tough time being in science, any science because your "ding dong phallus mind, sees a ellipse as another dick-penis, rather than a mind like AP's that sees ONLY SCIENCE TRUTH, SCIENCE REALITY,

2:19 PM (3 hours ago)

. dick-penis, rather than a mind like AP's that sees ONLY SCIENCE TRUTH, SCIENCE REALITY, sees only objectivity.



me (Archimedes Plutonium change)
4:43 PM (45 minutes ago)

kibo doing the soap bubble experiment in High School where girls screamed and cried

Kibo even failed comedy, let alone math and physics, yet tap dancing school in Boston was not fulfilling for the failure.
o-:^>___?
`~~c--^c'

Tootsie


On Monday, May 4, 2020 at 2:19:07 PM UTC-5, . wrote:
short for Kibo Parry Moroney

Post by Dan Christensen
"being gay" "gay sex" "sex pasture" "ding dong phallus mind"
"dick-penis" "dingdong followers" "bed warmers" "Bend over" "sex gigolos"
Looks like the only one here bringing up the subject of gay sex is you,
Plutonium. Are you obsessed with having gay sex with this "gang of 12"
of yours?
I assume you have evidence that these people are gay and that being gay
is somehow disruptive.

AP, the King of Science, reduced the worthless kibo Parry Moroney down to the vestiges of "."

If AP the King of Science destroys the kibo once again, there is no further lower place than that of "."

So I recommend a new name fake name for the failure Kibo Parry Moroney, the kibo failure, for he failed physics, he failed math, so why the hell is he even in sci.math or sci.physics? Why is he even here? Is it because the failure Kibo Parry Moroney uses sci.math and sci.physics as a gay pick up bar??? Is that his only reason for ever posting here at all-- he wants to pick up a gay???

So, here, kibo failure, here is your new next fake name--- kibo Poofster, or did you fail blowing soap bubbles also in Grade School class, instead of blowing soap bubbles in chemistry or physics class, kibo-- Poofster Moroney wanted to blow a wad of his cum semen sperm in a ejaculated bubble out of his poofster mouth. With a maraschino cherry on top. But the little Grade school girls sitting next to kibo in class started screaming and crying.

_ _/|
\'o.0'
=(___)=
U


Tootsie Comics, brought to you by tootsie in the Living Room LTD.


o-:^>___?
`~~c--^c'

Tootsie

[Michael Moroney]

Post by Archimedes Plutonium
Re: 2-Dan Christensen and Jan Burse, the arsewipes of Logic with their 2 OR
3 = 5 and their mind numbing belief a ellipse is a conic section when it never
was-- it was a cylinder section
8 posts by 5 authors
11:47 AM (5 hours ago)

Post by Archimedes Plutonium
an ellipse is a conic section Right. Want to see my proof again? Here's

an alternative proof based on Dandelin's spheres: http://www.nabla.hr/CO-ConicsProperties2.htm#Da

And here is Franz's excellent proof!

Below you will find a simple *proof* that shows that certain conic
sections are ellipses.

Some preliminaries:

Top view of the conic section and depiction of the coordinate system used
in the proof:

^ x
|
-+- <= x=h
.' | `.
. | .
| | |
' | '
`. | .'
y <----------+ <= x=0

Cone (side view):
.
/|\
/ | \
/b | \
/---+---' <= x = h
/ |' \
/ ' | \
/ ' | \
x = 0 => '-------+-------\
/ a | \

Proof:

r(x) = a - ((a-b)/h)x and d(x) = a - ((a+b)/h)x, hence

y(x)^2 = r(x)^2 - d(x)^2 = ab - ab(2x/h - 1)^2 = ab(1 - 4(x - h/2)^2/h^2.

Hence (1/ab)y(x)^2 + (4/h^2)(x - h/2)^2 = 1 ...equation of an ellipse

qed

[Mostowski Collapse]

Any progress Dan-O-Matik?

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
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]

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

No progress so far other than finding a fairly detailed informal proof by Arjun Jain to perhaps serve as a template for my formal proof.

https://arxiv.org/pdf/1207.6698.pdf


Dan

[Mostowski Collapse]

There is also:

Sur le théorème de Zorn
Nicolas Bourbaki
Archiv der Mathematik volume 2, pages 434–437 (1949)

But I didn't find a PDF yet.

Claude Chevalley from the Nicolas Bourbaki knew Zorn.

Post by Dan Christensen

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

No progress so far other than finding a fairly detailed informal proof by Arjun Jain to perhaps serve as a template for my formal proof.
https://arxiv.org/pdf/1207.6698.pdf
Dan

[Mostowski Collapse]

Arjun Jain does, with his function s dashed, he
maps a partial order to a kind of half Dedekind cuts,

s(x) ⊆ s(y) iff x =< y

The hypothesis of Zorns lemma basically says
that for each chain L there is an x such that
L ⊆ s(x). The non degenerate half Dedekind cuts have

this property also, even if they represent an
irrational number, there are rational numbers
above them. But the beginning of page 3 in

Arjun Jain is incoherent garbel, using undefined
notation C_x and suddently switching from =<
to some ⊆. The beginning of page 3 in Arjun Jain

has probably to be recast. Also after lemma 5
it makes a second proof using towers.

Post by Mostowski Collapse
Sur le théorème de Zorn
Nicolas Bourbaki
Archiv der Mathematik volume 2, pages 434–437 (1949)
But I didn't find a PDF yet.
Claude Chevalley from the Nicolas Bourbaki knew Zorn.

Post by Dan Christensen

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

No progress so far other than finding a fairly detailed informal proof by Arjun Jain to perhaps serve as a template for my formal proof.
https://arxiv.org/pdf/1207.6698.pdf
Dan

[Mostowski Collapse]

towers is a kind of generalized ordinal induction.
So it seems you need a lot of machinery here.

Post by Mostowski Collapse
Arjun Jain does, with his function s dashed, he
maps a partial order to a kind of half Dedekind cuts,
s(x) ⊆ s(y) iff x =< y
The hypothesis of Zorns lemma basically says
that for each chain L there is an x such that
L ⊆ s(x). The non degenerate half Dedekind cuts have
this property also, even if they represent an
irrational number, there are rational numbers
above them. But the beginning of page 3 in
Arjun Jain is incoherent garbel, using undefined
notation C_x and suddently switching from =<
to some ⊆. The beginning of page 3 in Arjun Jain
has probably to be recast. Also after lemma 5
it makes a second proof using towers.

Post by Mostowski Collapse
Sur le théorème de Zorn
Nicolas Bourbaki
Archiv der Mathematik volume 2, pages 434–437 (1949)
But I didn't find a PDF yet.
Claude Chevalley from the Nicolas Bourbaki knew Zorn.

Post by Dan Christensen

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)

No progress so far other than finding a fairly detailed informal proof by Arjun Jain to perhaps serve as a template for my formal proof.
https://arxiv.org/pdf/1207.6698.pdf
Dan

[Mostowski Collapse]

Ping Dan. Some progress?

Post by Dan Christensen
I am working on a proof of Zorn's Lemma using my DC Proof 2.0 freeware. (No promises!) There is some ambiguity in the Wikipedia article at https://en.wikipedia.org/wiki/Zorn%27s_lemma#Statement_of_the_lemma
Is the following a correct statement of Zorn's Lemma?
Where
Set(s) = s is a set
'&' = AND-operator
'|' = OR-operator
x in y = x is an element of y
ALL(s):[Set(s)
& EXIST(a):a in s (s is non-empty)
& ALL(a):[a in s => a<=a] (reflexity of <=)
& ALL(a):ALL(b):[a in s & b in s => [a<=b & b<=a => a=b]] (antisymmetry of <=)
& ALL(a):ALL(b):ALL(c):[a in s & b in s & c in s => [a<=b & b<=c => a<=c]] (transivity of <=)
& ALL(a):[Set(a) & ALL(b):[b in a => b in s] (subset of s)
& ALL(b):ALL(c):[b in a & c in a => b<=c | c<=b] (connexity of <= in a)
=> EXIST(b):[b in a & ALL(c):[c in a => c<=b]]] (boundedness of a)
=> EXIST(a):[a in s & ALL(b):[b in s => b<=a]]] (boundedness of s)
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]

Post by Mostowski Collapse
Ping Dan. Some progress?

Just playing around with various constructs that I might use. Don't know if it will lead to a finished proof, but having fun.

Now using an informal proof by J. Lewin as a model.


Dan

[Mostowski Collapse]

If you can prove ZL without AC,

than we know DC Proof is inconsistent.

Post by Dan Christensen

Post by Mostowski Collapse
Ping Dan. Some progress?

Just playing around with various constructs that I might use. Don't know if it will lead to a finished proof, but having fun.
Now using an informal proof by J. Lewin as a model.
Dan

[Dan Christensen]

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!

I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.


Dan

[Mostowski Collapse]

Thats the most crazy thing I have heard.
So you try proving ZL without AC?
You cannot prove axioms, if they are

independent. Trying to prove ZL, is
the same like trying to prove AC, since
the are logically equivalent over ZF.

Ever seen somebody prove AC?

https://en.wikipedia.org/wiki/Axiom_of_choice#Independence

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.
Dan

[Mostowski Collapse]

Or could it be that you don't get the
point of this chain of reasoning, and
what it means for proofs?

ZL and AC are logically equivalent over ZF
AC is independent of ZF
---------------------------------------------
ZL is independent of ZF

ZF=Zermelo Fraenkel set theory without AC
AC=Axiom of Choice
ZL=Zorns Lemma

Since ZL is independent of ZF, there is
no proof of ZL from ZF. That is what
independence means. !!NO PROOF!!

For example commutativity in a group
is independent from associativity.
You cannot prove it from associativity,

there are some groups, hence associative,
but not commutative, and there are some
groups, hence assoviative, but commutative.

This is what the famous prove by 1938,
Kurt Gödel and 1963, Paul Cohen convey for
another structure, not a group, but

a model of ZF, there are models of ZF
where AC holds, and there are models of
ZF where AC does not hold,

subsequently you cannot prove AC from ZF,
and since AC and ZL are logically equivalent,
you can also not prove ZL from ZF.

Ask MSE when you are not sure and want
reinvent the wheel. It took ca. 30 years
between Gödel and Cohen, to have a

full picture of the question. I really
recommend asking MSE (Math Stack Exchange)
whether ZL is provable from ZF, that

set theory without the axiom of choice.

Post by Mostowski Collapse
Thats the most crazy thing I have heard.
So you try proving ZL without AC?
You cannot prove axioms, if they are
independent. Trying to prove ZL, is
the same like trying to prove AC, since
the are logically equivalent over ZF.
Ever seen somebody prove AC?
https://en.wikipedia.org/wiki/Axiom_of_choice#Independence

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.
Dan

[Dan Christensen]

Post by Mostowski Collapse
Thats the most crazy thing I have heard.
So you try proving ZL without AC?
You cannot prove axioms, if they are
independent. Trying to prove ZL, is
the same like trying to prove AC, since
the are logically equivalent over ZF.
Ever seen somebody prove AC?

This is starting to sound really exciting! Will keep you posted if and when...


Dan

[h***@gmail.com]

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.

You do know that AC, ZL (and well-ordering) are all equivalent wrt. ZF. Right?

So don't invest too much time and effort in this fool's errand.

[Dan Christensen]

Post by h***@gmail.com

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.

You do know that AC, ZL (and well-ordering) are all equivalent wrt. ZF. Right?

So they say. It wasn't my intention to upset any apple carts, but SO FAR I don't see why AC is necessary to prove ZL. I may well discover why for myself very shortly.

Post by h***@gmail.com
So don't invest too much time and effort in this fool's errand.

Thank you for your concern.


Dan

[Mostowski Collapse]

Well you also don't see Coronavirus. Nevertheless
some people exercise social distancing, others
don't care or think Coronavirus is caused by 5G.

So its a matter whether you trust scientific 3rd
parties or not. Like whether you trust other
mathematcians and logicians what they have written

in math books. That ZL is independent from ZF
is a typical text book result, you find it in
every set theory text book one way or the other.

So there are Covidiots and there are ZFidiots.

LoL

Post by Dan Christensen

Post by h***@gmail.com

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.

You do know that AC, ZL (and well-ordering) are all equivalent wrt. ZF. Right?

So they say. It wasn't my intention to upset any apple carts, but SO FAR I don't see why AC is necessary to prove ZL. I may well discover why for myself very shortly.

Post by h***@gmail.com
So don't invest too much time and effort in this fool's errand.

Thank you for your concern.
Dan

[Mostowski Collapse]

Any progress proving Zorns lemma, without AC.
While you are it, maybe you can prove existence
of N, also without AOI, could be your

stroke of luck!!!

Post by Dan Christensen

Post by h***@gmail.com

Post by Dan Christensen

Post by Mostowski Collapse
If you can prove ZL without AC,
than we know DC Proof is inconsistent.

Or something else may be inconsistent. Cool!
I am currently trying to prove ZL without AC. It may well turn out to be another dead end. Maybe not. No promises.

You do know that AC, ZL (and well-ordering) are all equivalent wrt. ZF. Right?

So they say. It wasn't my intention to upset any apple carts, but SO FAR I don't see why AC is necessary to prove ZL. I may well discover why for myself very shortly.

Post by h***@gmail.com
So don't invest too much time and effort in this fool's errand.

Thank you for your concern.
Dan

[Me]

While you are [at] it <etc.>

[Dan Christensen]

Post by Mostowski Collapse
Any progress proving Zorns lemma, without AC.

For now, I will be using AC just to see precisely where if anywhere in the proof it is essential to always pick the SAME strict upper bound for a given chain in different instances. Currently on line 415 of the current draft.

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]

Well to original AC only postulates existence
of a transversal. There is no picking. There is
no global function c() that picks.

Also in your formulation you have exists c(),
this doesn't mean that even for the same instance
the same c() must be used.

Also Zorns Lemma only says there exists a maximum.
If there are multiple maximums, the condition
of existence is also satisfied,

and Zorns Lemma doesn't pick one of them.

Post by Dan Christensen

Post by Mostowski Collapse
Any progress proving Zorns lemma, without AC.

For now, I will be using AC just to see precisely where if anywhere in the proof it is essential to always pick the SAME strict upper bound for a given chain in different instances. Currently on line 415 of the current draft.
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]

AC is not global choice. Global choice is
stronger than AC. Glonbal choice would provide
you some picking on the level of a model

of ZFC. See for example:

3.9 On the existence of definable global choice
Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795

Post by Mostowski Collapse
Well to original AC only postulates existence
of a transversal. There is no picking. There is
no global function c() that picks.
Also in your formulation you have exists c(),
this doesn't mean that even for the same instance
the same c() must be used.
Also Zorns Lemma only says there exists a maximum.
If there are multiple maximums, the condition
of existence is also satisfied,
and Zorns Lemma doesn't pick one of them.

Post by Dan Christensen

Post by Mostowski Collapse
Any progress proving Zorns lemma, without AC.

For now, I will be using AC just to see precisely where if anywhere in the proof it is essential to always pick the SAME strict upper bound for a given chain in different instances. Currently on line 415 of the current draft.
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]

Post by Dan Christensen

Post by Mostowski Collapse
Any progress proving Zorns lemma, without AC.

For now, I will be using AC just to see precisely where if anywhere in the proof it is essential to always pick the SAME strict upper bound for a given chain in different instances. Currently on line 415 of the current draft.

Using AC, I have constructed the function f2: chx --> sx where chx is the set of chains on the set sx such that...


619 ALL(a):[a in chx => f2(a) in sx & ALL(b):[b in a => b<f2(a)]]
Conclusion, 613

Maybe half done?


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]

Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Post by Dan Christensen

Post by Dan Christensen

Post by Mostowski Collapse
Any progress proving Zorns lemma, without AC.

For now, I will be using AC just to see precisely where if anywhere in the proof it is essential to always pick the SAME strict upper bound for a given chain in different instances. Currently on line 415 of the current draft.

Using AC, I have constructed the function f2: chx --> sx where chx is the set of chains on the set sx such that...
619 ALL(a):[a in chx => f2(a) in sx & ALL(b):[b in a => b<f2(a)]]
Conclusion, 613
Maybe half done?
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]

Post by Mostowski Collapse
Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Taking a break. It's exhausting work. Every line of the informal proof is like a puzzle. One line simply claims the existence of the choice function. It took me about 600 lines to formally construct it. I had to start over several times.


Dan

[Mostowski Collapse]

Possibly the reason why many Proof assistants
have tactics for semi-automation:

How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-in-proof-assistants

Post by Dan Christensen

Post by Mostowski Collapse
Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Taking a break. It's exhausting work. Every line of the informal proof is like a puzzle. One line simply claims the existence of the choice function. It took me about 600 lines to formally construct it. I had to start over several times.
Dan

[Dan Christensen]

Post by Mostowski Collapse

Post by Dan Christensen

Post by Mostowski Collapse
Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Taking a break. It's exhausting work. Every line of the informal proof is like a puzzle. One line simply claims the existence of the choice function. It took me about 600 lines to formally construct it. I had to start over several times.

Possibly the reason why many Proof assistants
How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-in-proof-assistants

There are no "tactics" built into DC Proof. That would defeat the whole purpose of teaching students the basic methods of proof so they can write their own proofs, formal or otherwise.

IIUC these "tactics" are presently of very limited use in any case.


Dan

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

[Bobrù Nervózní]

Post by Dan Christensen

Post by Mostowski Collapse
How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-

in-proof-assistants

Post by Dan Christensen
There are no "tactics" built into DC Proof. That would defeat the whole
purpose of teaching students the basic methods of proof so they can
write their own proofs, formal or otherwise.
IIUC these "tactics" are presently of very limited use in any case. Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com Visit my
Math Blog at http://www.dcproof.wordpress.com

Irrelevant. Which can't stop you from stealing lemmas, axioms and models,
like there is no day tomorrow. You are paid by bill gates. He owns patents
on *other peoples* work on *gain-of-function* development on bat viruses
and afferent toxic damaging vaccines. You are no different from him, in
any way. Considering your age, depressing.

[Dan Christensen]

On Sunday, June 7, 2020 at 7:35:40 AM UTC-4, Bobrù Nervózní wrote:

Nervous Beaver???

Umm... Nice handle, soudruh!

But I think I will simply ignore you for now. Ahoj.

Dan

[Bobrù Nervózní]

Nervous Beaver??? Umm... Nice handle, soudruh!
But I think I will simply ignore you for now. Ahoj.

You don't even know when a lemma, axiom or theory has to have a
*mathematical beauty*. It takes decades of lab experience, to achieve
such that. But mathematicians are lab illiterates. No hope.

[Mostowski Collapse]

LoL, Dan-O-Matik got a czech admirer.

Guess what, this Bobrù Nervózní
is a complete crazy.

Post by Bobrù Nervózní

Nervous Beaver??? Umm... Nice handle, soudruh!
But I think I will simply ignore you for now. Ahoj.

You don't even know when a lemma, axiom or theory has to have a
*mathematical beauty*. It takes decades of lab experience, to achieve
such that. But mathematicians are lab illiterates. No hope.

[Mostowski Collapse]

Now you have two purposes teaching and
doing large proofs like Zorns lemma.

Somehow they are in conflict now. Since
your teaching seems to exclude tactics.

Looks like you have trapped yourself.

LMAO!

Post by Dan Christensen

Post by Mostowski Collapse

Post by Dan Christensen

Post by Mostowski Collapse
Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Taking a break. It's exhausting work. Every line of the informal proof is like a puzzle. One line simply claims the existence of the choice function. It took me about 600 lines to formally construct it. I had to start over several times.

Possibly the reason why many Proof assistants
How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-in-proof-assistants

There are no "tactics" built into DC Proof. That would defeat the whole purpose of teaching students the basic methods of proof so they can write their own proofs, formal or otherwise.
IIUC these "tactics" are presently of very limited use in any case.
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]

Before you continue shooting your own
foot, consider this: You could also teach
tactics. For example somebody doing matrix

inversion might use the Gauss elimination
step tactic. I don't see why tactics should
not be teachable? They are not basic, but

advanced, so for advanced teachning, you
could also tell your students something
about tactics. Tactis are also something

that can be teached. I says "dummies" here:

https://www.dummies.com/education/math/calculus/how-to-use-gaussian-elimination-to-solve-systems-of-equations/

A tactic is just a how-to. There are many
how-to to make larger proofs.

LoL

Post by Mostowski Collapse
Now you have two purposes teaching and
doing large proofs like Zorns lemma.
Somehow they are in conflict now. Since
your teaching seems to exclude tactics.
Looks like you have trapped yourself.
LMAO!

Post by Dan Christensen

Post by Mostowski Collapse

Post by Dan Christensen

Post by Mostowski Collapse
Hey Dan, its weekend. Time to do some interesting
work. More progress about Zorns lemma in DC Proof?

Taking a break. It's exhausting work. Every line of the informal proof is like a puzzle. One line simply claims the existence of the choice function. It took me about 600 lines to formally construct it. I had to start over several times.

Possibly the reason why many Proof assistants
How do 'tactics' work in proof assistants?
https://cstheory.stackexchange.com/questions/5696/how-do-tactics-work-in-proof-assistants

There are no "tactics" built into DC Proof. That would defeat the whole purpose of teaching students the basic methods of proof so they can write their own proofs, formal or otherwise.
IIUC these "tactics" are presently of very limited use in any case.
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]

Post by Mostowski Collapse
Now you have two purposes teaching and
doing large proofs like Zorns lemma.

I do these larger proofs for fun and to demonstrate the capability of DC Proof. I don't really think students will use it for more than a few hours to get the idea of what a proof actually is and to learn the basic rules of logic which are rarely spelled out effectively anywhere. But it's good for them to see that DC Proof is capable of some heavy lifting if necessary. Past a certain level of complexity, of course, it's just not feasible to do a formal proof. Not unless you are a fanatic like me!


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]

I don't think you can do heavy lifting without
tactics. Thats like writing assembler by hand.
Historically people didn't have FORTRAN. So
when they wanted to compute:

c=sqrt(a^2+b^2);

They needed to code in assembler. FORTRAN litterally
means FORmula TRANslation. So Humans invented
compilers, so that somebody can more natural
input programs. Its the same with tactics, its

there to allow you to do heavy lifting.

Fortran (/ˈfɔːrtræn/; formerly FORTRAN, derived from Formula Translation[2])
https://en.wikipedia.org/wiki/Fortran

For example instead of re-doing multiple times 600 lines
proof, just because something small changed,
encapsulate what the 600 lines do in a tactic, and
just apply the tactic.

Post by Dan Christensen

Post by Mostowski Collapse
Now you have two purposes teaching and
doing large proofs like Zorns lemma.

I do these larger proofs for fun and to demonstrate the capability of DC Proof. I don't really think students will use it for more than a few hours to get the idea of what a proof actually is and to learn the basic rules of logic which are rarely spelled out effectively anywhere. But it's good for them to see that DC Proof is capable of some heavy lifting if necessary. Past a certain level of complexity, of course, it's just not feasible to do a formal proof. Not unless you are a fanatic like me!
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]

Post by Mostowski Collapse
I don't think you can do heavy lifting without
tactics.

I thought the Cantor-Bernstein-Schroeder Theorem was a bit of heavy lifting. See my proof: http://dcproof.com/CBS.htm

Post by Mostowski Collapse
Thats like writing assembler by hand.

Some programmers do just that.


Dan

[Mostowski Collapse]

With tactics, here "blast", its only:

subsection {* The Schröder-Berstein Theorem *}

lemma disj_lemma: "- (f ` X) = g ` (-X) ==> f a = g b ==> a ∈ X ==> b ∈ X"
by blast

lemma surj_if_then_else:
"-(f ` X) = g ` (-X) ==> surj (λz. if z ∈ X then f z else g z)"
by (simp add: surj_def) blast

lemma bij_if_then_else:
"inj_on f X ==> inj_on g (-X) ==> -(f ` X) = g ` (-X) ==>
h = (λz. if z ∈ X then f z else g z) ==> inj h ∧ surj h"
apply (unfold inj_on_def)
apply (simp add: surj_if_then_else)
apply (blast dest: disj_lemma sym)
done

lemma decomposition: "∃X. X = - (g ` (- (f ` X)))"
apply (rule exI)
apply (rule lfp_unfold)
apply (rule monoI, blast)
done

theorem Schroeder_Bernstein:
"inj (f :: 'a => 'b) ==> inj (g :: 'b => 'a)
==> ∃h:: 'a => 'b. inj h ∧ surj h"
apply (rule decomposition [where f=f and g=g, THEN exE])
apply (rule_tac x = "(λz. if z ∈ x then f z else inv g z)" in exI)
--{*The term above can be synthesized by a sufficiently detailed proof.*}
apply (rule bij_if_then_else)
apply (rule_tac [4] refl)
apply (rule_tac [2] inj_on_inv_into)
apply (erule subset_inj_on [OF _ subset_UNIV])
apply blast
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
done

https://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/HOL-ex/Set_Theory.html

Post by Dan Christensen

Post by Mostowski Collapse
I don't think you can do heavy lifting without
tactics.

I thought the Cantor-Bernstein-Schroeder Theorem was a bit of heavy lifting. See my proof: http://dcproof.com/CBS.htm

Post by Mostowski Collapse
Thats like writing assembler by hand.

Some programmers do just that.
Dan

[Mostowski Collapse]

What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

Like can we for example proof:

p => p

And then reuse such a lemma to prove:

q(x) => q(x) ?

Isabelle/HOL can do such things. It
seems metamath has also such a feature.
But DC Proof? It explicitly disallows predicate
quantifiers, but has function quantifiers.

Whats the language for tactics?

Post by Mostowski Collapse
subsection {* The Schröder-Berstein Theorem *}
lemma disj_lemma: "- (f ` X) = g ` (-X) ==> f a = g b ==> a ∈ X ==> b ∈ X"
by blast
"-(f ` X) = g ` (-X) ==> surj (λz. if z ∈ X then f z else g z)"
by (simp add: surj_def) blast
"inj_on f X ==> inj_on g (-X) ==> -(f ` X) = g ` (-X) ==>
h = (λz. if z ∈ X then f z else g z) ==> inj h ∧ surj h"
apply (unfold inj_on_def)
apply (simp add: surj_if_then_else)
apply (blast dest: disj_lemma sym)
done
lemma decomposition: "∃X. X = - (g ` (- (f ` X)))"
apply (rule exI)
apply (rule lfp_unfold)
apply (rule monoI, blast)
done
"inj (f :: 'a => 'b) ==> inj (g :: 'b => 'a)
==> ∃h:: 'a => 'b. inj h ∧ surj h"
apply (rule decomposition [where f=f and g=g, THEN exE])
apply (rule_tac x = "(λz. if z ∈ x then f z else inv g z)" in exI)
--{*The term above can be synthesized by a sufficiently detailed proof.*}
apply (rule bij_if_then_else)
apply (rule_tac [4] refl)
apply (rule_tac [2] inj_on_inv_into)
apply (erule subset_inj_on [OF _ subset_UNIV])
apply blast
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
done
https://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/HOL-ex/Set_Theory.html

Post by Dan Christensen

Post by Mostowski Collapse
I don't think you can do heavy lifting without
tactics.

I thought the Cantor-Bernstein-Schroeder Theorem was a bit of heavy lifting. See my proof: http://dcproof.com/CBS.htm

Post by Mostowski Collapse
Thats like writing assembler by hand.

Some programmers do just that.
Dan

[Dan Christensen]

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates. AFAICT it was not something that comes up in math textbooks. A needless complication for my target audience. Tried to avoid feature creep.


Dan

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

[Jim Burns]

On Sunday, June 7, 2020 at 12:33:36 PM UTC-4,

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates.

Am I correct to think that, at least at some earlier point,
your DCProof quantified over functions?

Functions are similar to predicates in important ways.

Let B be some set.

Compare how we represent a predicate P on BxBxB and
a function f: BxB -> B

They're both subsets of BxBxB. The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.

If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"

We've written the (variable) predicate as
a statement about a (variable) function, f(x,y) = b.

AFAICT it was not something that comes up in math textbooks.
A needless complication for my target audience.
Tried to avoid feature creep.

Some features make things less complicated.

[Dan Christensen]

Post by Jim Burns

On Sunday, June 7, 2020 at 12:33:36 PM UTC-4,

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates.

Am I correct to think that, at least at some earlier point,
your DCProof quantified over functions?

Yes.

Post by Jim Burns
Functions are similar to predicates in important ways.

In DC Proof, a distinction is made. Function and variable names start with a lower-case letter, were predicate and proposition names begin with an upper-case letter.

Post by Jim Burns
Let B be some set.
Compare how we represent a predicate P on BxBxB and
a function f: BxB -> B
They're both subsets of BxBxB.

If P is a predicate, it cannot be a subset in DC Proof. You cannot have P=f.

Post by Jim Burns
The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.
If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Not in DC Proof.

Post by Jim Burns
Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

Not in DC Proof.

Post by Jim Burns
If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"
We've written the (variable) predicate as
a statement about a (variable) function, f(x,y) = b.

AFAICT it was not something that comes up in math textbooks.
A needless complication for my target audience.
Tried to avoid feature creep.

Some features make things less complicated.

If quantification of propositions and predicates was a common feature in math textbooks, I would have included it. But it isn't and I didn't. Thanks anyway.


Dan

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

[Jim Burns]

On Sunday, June 7, 2020 at 1:58:12 PM UTC-4,

Post by Jim Burns

On Sunday, June 7, 2020 at 12:33:36 PM UTC-4,

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or
predicates.

Am I correct to think that, at least at some earlier point,
your DCProof quantified over functions?

Yes.

Post by Jim Burns
Functions are similar to predicates in important ways.

In DC Proof, a distinction is made.

You're describing a distinction between how they're _written_

Functions can be replaced by predicates.

Suppose we have two functions f and g, and we want to write
g(f(x)) = y

That's a nice, compact, easily understandable notation --
a good example of a feature that makes things less complicated.

HOWEVER, we could still write something meaning the same thing
without functions -- with only predicates that mean what
a function means.

Define

F(x,u) <-> f(x) = u

G(v,y) <-> g(v) = y

Because F and G are _function-like_ we need to require
forall x, exists unique u, F(x,u)
forall v, exists unique y, G(v,y)

That's what we implicitly say when we use function notation.

Given that understanding, we can write this:
( g(f(x)) = y ) <->
exists u,( F(x,u) & G(u,y) )

In a certain sense, functions are special predicates.
These special function-like predicates allow us to use
function notation, which expresses what we want to say much
more clearly. That's a good thing, but it's not _required_

Function and variable names start with a lower-case letter,
were predicate and proposition names begin with an
upper-case letter.

Post by Jim Burns
Let B be some set.
Compare how we *represent* a predicate P on BxBxB and
a function f: BxB -> B

*Emphasis added*

Post by Jim Burns
They're both subsets of BxBxB.

If P is a predicate, it cannot be a subset in DC Proof.
You cannot have P=f.

I have a strong suspicion that, even in DCProof, you can have
a subset 'P' which represents predicate P and a subset 'f'
which represents a function f such that 'P' = 'f'.

However, that wasn't my point.

Is it possible to have P(x,y) <-> (f(x,y) = b)
in DCProof? That was my point.

Post by Jim Burns
The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.
If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Not in DC Proof.

Post by Jim Burns
Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

Not in DC Proof.

Post by Jim Burns
If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"
We've written the (variable) predicate as
a statement about a (variable) function, f(x,y) = b.

AFAICT it was not something that comes up in math textbooks.
A needless complication for my target audience.
Tried to avoid feature creep.

Some features make things less complicated.

If quantification of propositions and predicates was a
common feature in math textbooks, I would have included it.

Whatever your reasons were, you _in effect_ included it.

A variable over functions can be used to say the same thing
you would say using a variable over predicates.
Where you would other wise say
"For all x, y, for all predicates P(x,y), ..."
say
"For all x, y, for all f(x,y) = b, ... "

But it isn't and I didn't. Thanks anyway.

[Mostowski Collapse]

If DC Proof would also allow predicate
quantification, it would be too obvious that
it is inconsistent. Because DC Proof doesn't

have type security that would guard these
quantifiers. It has self application, which
violates the usual type security.

Post by Jim Burns

On Sunday, June 7, 2020 at 1:58:12 PM UTC-4,

Post by Jim Burns

On Sunday, June 7, 2020 at 12:33:36 PM UTC-4,

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or
predicates.

Am I correct to think that, at least at some earlier point,
your DCProof quantified over functions?

Yes.

Post by Jim Burns
Functions are similar to predicates in important ways.

In DC Proof, a distinction is made.

You're describing a distinction between how they're _written_
Functions can be replaced by predicates.
Suppose we have two functions f and g, and we want to write
g(f(x)) = y
That's a nice, compact, easily understandable notation --
a good example of a feature that makes things less complicated.
HOWEVER, we could still write something meaning the same thing
without functions -- with only predicates that mean what
a function means.
Define
F(x,u) <-> f(x) = u
G(v,y) <-> g(v) = y
Because F and G are _function-like_ we need to require
forall x, exists unique u, F(x,u)
forall v, exists unique y, G(v,y)
That's what we implicitly say when we use function notation.
( g(f(x)) = y ) <->
exists u,( F(x,u) & G(u,y) )
In a certain sense, functions are special predicates.
These special function-like predicates allow us to use
function notation, which expresses what we want to say much
more clearly. That's a good thing, but it's not _required_

Function and variable names start with a lower-case letter,
were predicate and proposition names begin with an
upper-case letter.

Post by Jim Burns
Let B be some set.
Compare how we *represent* a predicate P on BxBxB and
a function f: BxB -> B

*Emphasis added*

Post by Jim Burns
They're both subsets of BxBxB.

If P is a predicate, it cannot be a subset in DC Proof.
You cannot have P=f.

I have a strong suspicion that, even in DCProof, you can have
a subset 'P' which represents predicate P and a subset 'f'
which represents a function f such that 'P' = 'f'.
However, that wasn't my point.
Is it possible to have P(x,y) <-> (f(x,y) = b)
in DCProof? That was my point.

Post by Jim Burns
The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.
If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Not in DC Proof.

Post by Jim Burns
Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

Not in DC Proof.

Post by Jim Burns
If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"
We've written the (variable) predicate as
a statement about a (variable) function, f(x,y) = b.

AFAICT it was not something that comes up in math textbooks.
A needless complication for my target audience.
Tried to avoid feature creep.

Some features make things less complicated.

If quantification of propositions and predicates was a
common feature in math textbooks, I would have included it.

Whatever your reasons were, you _in effect_ included it.
A variable over functions can be used to say the same thing
you would say using a variable over predicates.
Where you would other wise say
"For all x, y, for all predicates P(x,y), ..."
say
"For all x, y, for all f(x,y) = b, ... "

But it isn't and I didn't. Thanks anyway.

[Dan Christensen]

Post by Jim Burns

On Sunday, June 7, 2020 at 1:58:12 PM UTC-4,

Post by Jim Burns

On Sunday, June 7, 2020 at 12:33:36 PM UTC-4,

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or
predicates.

Am I correct to think that, at least at some earlier point,
your DCProof quantified over functions?

Yes.

Post by Jim Burns
Functions are similar to predicates in important ways.

In DC Proof, a distinction is made.

You're describing a distinction between how they're _written_
Functions can be replaced by predicates.
Suppose we have two functions f and g, and we want to write
g(f(x)) = y
That's a nice, compact, easily understandable notation --
a good example of a feature that makes things less complicated.
HOWEVER, we could still write something meaning the same thing
without functions -- with only predicates that mean what
a function means.
Define
F(x,u) <-> f(x) = u
G(v,y) <-> g(v) = y
Because F and G are _function-like_ we need to require
forall x, exists unique u, F(x,u)
forall v, exists unique y, G(v,y)
That's what we implicitly say when we use function notation.
( g(f(x)) = y ) <->
exists u,( F(x,u) & G(u,y) )
In a certain sense, functions are special predicates.
These special function-like predicates allow us to use
function notation, which expresses what we want to say much
more clearly. That's a good thing, but it's not _required_

You can construct a function f using a predicate F in DC Proof, but that doesn't mean that f=F and that they are interchangeable in formal proofs.


Dan

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

Post by Jim Burns

Function and variable names start with a lower-case letter,
were predicate and proposition names begin with an
upper-case letter.

Post by Jim Burns
Let B be some set.
Compare how we *represent* a predicate P on BxBxB and
a function f: BxB -> B

*Emphasis added*

Post by Jim Burns
They're both subsets of BxBxB.

If P is a predicate, it cannot be a subset in DC Proof.
You cannot have P=f.

I have a strong suspicion that, even in DCProof, you can have
a subset 'P' which represents predicate P and a subset 'f'
which represents a function f such that 'P' = 'f'.
However, that wasn't my point.
Is it possible to have P(x,y) <-> (f(x,y) = b)
in DCProof? That was my point.

Post by Jim Burns
The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.
If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Not in DC Proof.

Post by Jim Burns
Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

Not in DC Proof.

Post by Jim Burns
If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"
We've written the (variable) predicate as
a statement about a (variable) function, f(x,y) = b.

AFAICT it was not something that comes up in math textbooks.
A needless complication for my target audience.
Tried to avoid feature creep.

Some features make things less complicated.

If quantification of propositions and predicates was a
common feature in math textbooks, I would have included it.

Whatever your reasons were, you _in effect_ included it.
A variable over functions can be used to say the same thing
you would say using a variable over predicates.
Where you would other wise say
"For all x, y, for all predicates P(x,y), ..."
say
"For all x, y, for all f(x,y) = b, ... "

But it isn't and I didn't. Thanks anyway.

[Me]

Post by Jim Burns
Functions are similar to predicates in important ways.

Actually, in the context of set theory, they usually aren't. (Please, read on.)

Post by Jim Burns
Let B be some set.
Compare how we represent a predicate P on BxBxB

Huh?! Seems to me that you are talking about a (set-theoretic) /relation/ (instead of a logical /predicate/) here.

See the notion of "predicate" here:
https://en.wikipedia.org/wiki/First-order_logic

Post by Jim Burns
and a function f: BxB -> B
They're both subsets of BxBxB.

See comment from above.

Post by Jim Burns
The difference is that we
place further conditions on the subset that represents f.
For all (x,y) e BxB, there exists a unique z e B such that
(x,y,z) e 'f'.

Exactly. Certain relations are functions (in the context of set theory).

Post by Jim Burns
If we're using function-valued variables, we also have
predicate-valued variables _in effect_

Again: "predicate" => "relation".

Post by Jim Burns
Suppose I want to write
"Forall predicates P on BxB, blahblah(P(x,y))"

=> Forall relations P on BxB, blahblah(P(x,y))

Post by Jim Burns
If I had function-valued variables, I could write
"Forall functions f from BxB to B, constant b e B,
(f(x,y) = b) -> blahblah(f(x,y) = b)"

Right. Of course.

Post by Jim Burns

Post by Dan Christensen
Tried to avoid feature creep.

Some features make things less complicated.

Sure. But one has to be careful (especially in the context of a formal system) not to "introduce" contradictions this way.

See: https://projecteuclid.org/download/pdf_1/euclid.bams/1183504091
for example.

[Mostowski Collapse]

Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."

Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.

From p->p, you can infer x=3->x=3.
https://en.wikipedia.org/wiki/Substitution_%28logic%29#Definition

Post by Dan Christensen

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates. AFAICT it was not something that comes up in math textbooks. A needless complication for my target audience. Tried to avoid feature creep.
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]

Sometime its called lifting-lemma.

Oh, you were talking about "heavy lifting",
and you don't know the lifting-lemma?

How ironic.

LoL

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.
https://en.wikipedia.org/wiki/Substitution_%28logic%29#Definition

Post by Dan Christensen

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates. AFAICT it was not something that comes up in math textbooks. A needless complication for my target audience. Tried to avoid feature creep.
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]

The lifting lemma is very easy. Let Φ
be a substitution, and lets the following
derivation be valid:

G |- A

Then this derivation is also valid:

GΦ |- AΦ

Φ might also replace propositional variables.
Maybe logicians should rename it to heavy-lifting-
lemma. But its a lemma from

meta mathematics. You usually prove it before
you prove cut elimination. So it might be also
found in the writings of Gentzen.

Post by Mostowski Collapse
Sometime its called lifting-lemma.
Oh, you were talking about "heavy lifting",
and you don't know the lifting-lemma?
How ironic.
LoL

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.
https://en.wikipedia.org/wiki/Substitution_%28logic%29#Definition

Post by Dan Christensen

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates. AFAICT it was not something that comes up in math textbooks. A needless complication for my target audience. Tried to avoid feature creep.
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]

The lifting-lemma doesn't need any quantifiers.
It only assumes a derivation G |- A, and it
says that you can lift this derivation

GΦ |- AΦ. When this is meta-mathematically
valid, then you could of course also offer such
an inference rule. If our system does

not have such an inference rule, it might
still exist as a tactic. A tactic can realize
an admissible rule, it can do the necessary

proof transformation, in a purist setting where
the corresponding substitution instances are not
direcly available in the given calculus,

"In logic, a rule of inference is admissible
in a formal system if the set of theorems of
the system does not change when that rule is
added to the existing rules of the system.
In other words, every formula that can be
derived using that rule is already derivable
without that rule, so, in a sense, it is
redundant. The concept of an admissible rule
was introduced by Paul Lorenzen (1955)."
https://en.wikipedia.org/wiki/Admissible_rule

FORTRAN is also redundant, because you can
program in assembler. Nevertheless its a success
story. The same with tactics. It helps

giving back to the user of a Proof assistant,
what the user would anyway do as a human. Humans
easiy use admissible rules, when they see

that they are valid. Most of mathematical practice
is not crawling on assembler level of micro
inference rules, a lot of higher level macro

inference rules are used in daily business of
a methematician.

Post by Mostowski Collapse
The lifting lemma is very easy. Let Φ
be a substitution, and lets the following
G |- A
GΦ |- AΦ
Φ might also replace propositional variables.
Maybe logicians should rename it to heavy-lifting-
lemma. But its a lemma from
meta mathematics. You usually prove it before
you prove cut elimination. So it might be also
found in the writings of Gentzen.

Post by Mostowski Collapse
Sometime its called lifting-lemma.
Oh, you were talking about "heavy lifting",
and you don't know the lifting-lemma?
How ironic.
LoL

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.
https://en.wikipedia.org/wiki/Substitution_%28logic%29#Definition

Post by Dan Christensen

Post by Mostowski Collapse
What would be the potential of classes to realize
tactics, especially when one targets anyway
set theory? Does DC Proof have some
propositional variable substitution rule.

No. DC Proof does not quantify over propositions or predicates. AFAICT it was not something that comes up in math textbooks. A needless complication for my target audience. Tried to avoid feature creep.
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Me]

Post by Mostowski Collapse
"In logic, a rule of inference i
in a formal system if the set of theorems of
the system does not change when that rule is
added to the existing rules of the system.
In other words, every formula that can be
derived using that rule is already derivable
without that rule, so, in a sense, it is
redundant. The concept of an admissible rule
was introduced by Paul Lorenzen (1955)."
https://en.wikipedia.org/wiki/Admissible_rule

I guess that's what other authors (later) called "derived rules". Nice.

It would certainly be a very valuable feature if DC Proof would to _extend_ the set of rules of derivation by "derived rules".

For example, it's possible to derive the theorem

(P -> Q) -> ((Q -> R) -> (P -> R))

in the context of propositional logic. In some systems we can even derive the theorem schema:

(A -> B) -> ((B -> C) -> (A -> C)) .

From this it is clear that we might formulate the "derived rule":

phi -> psi
psi -> chi
----------
phi -> chi ,

which might be called the "chain rule" (CR).

Then this rule could be used in the course of a proof the following way:

:
(n) X -> Y
:
(m) Y -> Z
:
(o) X -> Z by CR
:

where X, Y, Z are just some wffs.

This feature certainly would simplify many of Dan's proofs considerably!

In the same way we might allow for the introduction of proved theorems as "additional axioms". We might even formulate that using the notion from above:

For each and every theorem phi of our system

---
phi

is a "derived rule". We might just label the theorems of our system and use these lables when referring to the related derived rules, preceded by the term "theorem introduction" (TI) in each case.

Post by Mostowski Collapse
Most of mathematical practice is not crawling on assembler level of micro
inference rules, a lot of higher level macro inference rules are used in
daily business of a mathematician.

Indeed! A tool like DC Proof might profit from the feature to extend the set of rules by "derived rules" (and especially "theorem introduction") considerably too.

[Me]

Post by Me

Post by Mostowski Collapse
"In logic, a rule of inference i
in a formal system if the set of theorems of
the system does not change when that rule is
added to the existing rules of the system.
In other words, every formula that can be
derived using that rule is already derivable
without that rule, so, in a sense, it is
redundant. The concept of an admissible rule
was introduced by Paul Lorenzen (1955)."
https://en.wikipedia.org/wiki/Admissible_rule

I guess that's what other authors (later) called "derived rules". Nice.

Ah, not quite:

"Every derivable rule is admissible, but not vice versa in general. A logic is structurally complete if every admissible rule is derivable."

Well, at least "Classical propositional calculus (CPC) is structurally complete."

Anyway, what I wrote in my post was related to "derivable rules".

[Dan Christensen]

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.

In DC Proof, it is built in:


1 P
Premise

2 P => P
Conclusion, 1


If x and 3 were introduced on line 1, we could have


2 x=3
Premise

3 x=3 => x=3
Conclusion, 2

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]

Yes if you have a proof:

G |- A

Then there is also a proof:

GΦ |- AΦ

Thats the lifting lemma of meta mathematics.

Now make it into a tactic, can you do this in DC Proof?

Post by Dan Christensen

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.

1 P
Premise
2 P => P
Conclusion, 1
If x and 3 were introduced on line 1, we could have
2 x=3
Premise
3 x=3 => x=3
Conclusion, 2
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]

The proof would look like this:

1 P
Premise

2 P => P
Conclusion, 1


3 x=3 => x=3
Tactic, 2

Post by Mostowski Collapse
G |- A
GΦ |- AΦ
Thats the lifting lemma of meta mathematics.
Now make it into a tactic, can you do this in DC Proof?

Post by Dan Christensen

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.

1 P
Premise
2 P => P
Conclusion, 1
If x and 3 were introduced on line 1, we could have
2 x=3
Premise
3 x=3 => x=3
Conclusion, 2
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]

The lifting lemma is mentioned as standard lifting
lemma [Lo78] in Principles of Automated Theorem Proving
David A. Duffy.

But I cannot decipher what Lo78 means since
I cannot find a PDF of Duffy.

Also HOL/Isabelle has another interpretation of the
name lifting lemma, although it is related. Other
variants are, not showing substitution:

A -> B
--------------------
(C -> A) -> (C -> B)

A -> B
------------------------
forall x A -> forall x B

The above is from Isabelle: A Generic Theorem Prover
von Lawrence C. Paulson. We also find this
here in normal modal logic:

A -> B
------------
[] A -> [] B

Just use Necessitation rule and Kripke schema.
https://en.wikipedia.org/wiki/Normal_modal_logic

Post by Mostowski Collapse
1 P
Premise
2 P => P
Conclusion, 1
3 x=3 => x=3
Tactic, 2

Post by Mostowski Collapse
G |- A
GΦ |- AΦ
Thats the lifting lemma of meta mathematics.
Now make it into a tactic, can you do this in DC Proof?

Post by Dan Christensen

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.

1 P
Premise
2 P => P
Conclusion, 1
If x and 3 were introduced on line 1, we could have
2 x=3
Premise
3 x=3 => x=3
Conclusion, 2
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Me]

My guess:

D. Loveland. Automated Theorem Proving - A Logical Basis. North Holland, 1978.

[Mostowski Collapse]

Prolog code for lifting:

subst((P->Q), S, T, (U->V)) :- !,
subst(P, S, T, U),
subst(Q, S, T, V).
subst(P, P, Q, Q) :- !.
subst(P, _, _, P).

lift('ax-1'(P), S, T, 'ax-1'(Q)) :- subst(P, S, T, Q).
lift('ax-2'(P), S, T, 'ax-2'(Q)) :- subst(P, S, T, Q).
lift('ax-mp'(P,Q), S, T, 'ax-mp'(U,V)) :-
lift(P, S, T, U),
lift(Q, S, T, V).

Example runs:

?- P = 'ax-mp'('ax-mp'('ax-2'(((p -> (u -> p) -> p)
-> (p -> u -> p) -> p -> p)), 'ax-1'((p -> (u -> p)
-> p))), 'ax-1'((p -> u -> p))), show(P, 0, _, _).

1. ax-2 (p -> (u -> p) -> p) -> (p -> u -> p) -> p -> p
2. ax-1 p -> (u -> p) -> p
3. ax-mp 1, 2 (p -> u -> p) -> p -> p
4. ax-1 p -> u -> p
5. ax-mp 3, 4 p -> p

?- P = 'ax-mp'('ax-mp'('ax-2'(((p -> (u -> p) -> p)
-> (p -> u -> p) -> p -> p)), 'ax-1'((p -> (u -> p)
-> p))), 'ax-1'((p -> u -> p))), lift(P, p, (r->s), Q),
show(Q, 0, _, _).

1. ax-2 ((r -> s) -> (u -> r -> s) -> r -> s)
-> ((r -> s) -> u -> r -> s) -> (r -> s) -> r -> s
2. ax-1 (r -> s) -> (u -> r -> s) -> r -> s
3. ax-mp 1, 2 ((r -> s) -> u -> r -> s) -> (r -> s) -> r -> s
4. ax-1 (r -> s) -> u -> r -> s
5. ax-mp 3, 4 (r -> s) -> r -> s

Post by Mostowski Collapse
The lifting lemma is mentioned as standard lifting
lemma [Lo78] in Principles of Automated Theorem Proving
David A. Duffy.
But I cannot decipher what Lo78 means since
I cannot find a PDF of Duffy.
Also HOL/Isabelle has another interpretation of the
name lifting lemma, although it is related. Other
A -> B
--------------------
(C -> A) -> (C -> B)
A -> B
------------------------
forall x A -> forall x B
The above is from Isabelle: A Generic Theorem Prover
von Lawrence C. Paulson. We also find this
A -> B
------------
[] A -> [] B
Just use Necessitation rule and Kripke schema.
https://en.wikipedia.org/wiki/Normal_modal_logic

Post by Mostowski Collapse
1 P
Premise
2 P => P
Conclusion, 1
3 x=3 => x=3
Tactic, 2

Post by Mostowski Collapse
G |- A
GΦ |- AΦ
Thats the lifting lemma of meta mathematics.
Now make it into a tactic, can you do this in DC Proof?

Post by Dan Christensen

Post by Mostowski Collapse
Dan-O-Matik hallucinates; "AFAICT it was not something
that comes up in math textbooks."
Well it is standard, maybe not in ultra dumbo land
canada where bigfoots are roaming.
From p->p, you can infer x=3->x=3.

1 P
Premise
2 P => P
Conclusion, 1
If x and 3 were introduced on line 1, we could have
2 x=3
Premise
3 x=3 => x=3
Conclusion, 2
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Me]

Post by Dan Christensen
No. DC Proof does not quantify over propositions or predicates. AFAICT it was
not something that comes up in math textbooks.

Right. Quantification over propositions is rarely mentioned, even in logic textbooks, and quantification over predicates would mean 2OL. Both systems aren't FOPL.

See: https://plato.stanford.edu/entries/quantification/#SecOrdQua
and: https://plato.stanford.edu/entries/quantification/#ProQua

You shouldn't "discuss" such topics with our local village idiot.

You know, this crank repeatedly claimed that Frege developed a system of FOPL in his /Begriffschrift/, what a moron.

Hint: "Frege's Begriffsschrift develops a formal system, which includes axioms for quantification over individual objects and concepts. For Frege, objects are the appropriate values for singular variables, and a concept is what is referred to by a predicate. Notice that despite Frege's use of the term, concepts, for him, are nothing like mental constructs, but rather objective constituents of the world. In particular, concepts are functions, which map objects into truth values. Since a predicate like “is extended” is true of some objects and false of others, Frege takes the concept /being extended/ to assign truth to an object if, and only if, it is extended.

Frege’s system is an axiomatization of what has come to be known as second-order logic, which is an important extension of classical quantificational logic. Hilbert & Ackermann (1928) contains the first axiomatic treatment of quantificational logic as a subject of its own, which they called “the narrower functional calculus”."

Source: https://plato.stanford.edu/entries/quantification

To make a long story short, the logical systems of that time were "higher-order".

"The logical systems within which Frege, Schröder, Russell, Zermelo
and other early mathematical logicians worked were all higher-order.

It was not until the 1910s that first-order logic was even distinguished
as a subsystem of higher-order logic."

Source: Matti Eklund, ON HOW LOGIC BECAME FIRST-ORDER
https://pdfs.semanticscholar.org/f323/efd2149ecb3075d8ccbbf6e07363c0b1f91a.pdf

[Dan Christensen]

Post by Mostowski Collapse
subsection {* The Schröder-Berstein Theorem *}
lemma disj_lemma: "- (f ` X) = g ` (-X) ==> f a = g b ==> a ∈ X ==> b ∈ X"
by blast
"-(f ` X) = g ` (-X) ==> surj (λz. if z ∈ X then f z else g z)"
by (simp add: surj_def) blast
"inj_on f X ==> inj_on g (-X) ==> -(f ` X) = g ` (-X) ==>
h = (λz. if z ∈ X then f z else g z) ==> inj h ∧ surj h"
apply (unfold inj_on_def)
apply (simp add: surj_if_then_else)
apply (blast dest: disj_lemma sym)
done
lemma decomposition: "∃X. X = - (g ` (- (f ` X)))"
apply (rule exI)
apply (rule lfp_unfold)
apply (rule monoI, blast)
done
"inj (f :: 'a => 'b) ==> inj (g :: 'b => 'a)
==> ∃h:: 'a => 'b. inj h ∧ surj h"
apply (rule decomposition [where f=f and g=g, THEN exE])
apply (rule_tac x = "(λz. if z ∈ x then f z else inv g z)" in exI)
--{*The term above can be synthesized by a sufficiently detailed proof.*}
apply (rule bij_if_then_else)
apply (rule_tac [4] refl)
apply (rule_tac [2] inj_on_inv_into)
apply (erule subset_inj_on [OF _ subset_UNIV])
apply blast
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
done

Heavy lifting for sure!

I, too, broke the proof into several lemmas (6 links on the main page, lines 5-10). http://dcproof.com/CBS.htm


Dan

[bassam karzeddin]

Relax Dan C. Troll since Zam's Lemma is also nonsese

Nobody can do anything meaningful in truly discovered mathematics munless (she/he) well-understand what is truly a real number fact

However, the rest is purely eingineering works which isn't mathematics at all, but approximation practical problems solutions for little earthy daily problems which is acceptable

A very famous and of an oldest and well standing eingineering problem is calculating a circle area by endless approximation where this is acceptable
and would last for ever with no end

But in pure and true mathematics, this is never any existing problem due to the well-proven fact that circle is a non-existing object both on the physical universal fact and theoretical facts as well, but what does exist is regular existing polygons that seems to you like a circle (Ref. my many public published posts in this regard)

Leave the eingineering problems for other engineering fields for what so ever reasons (mathematicians, philosophers, logicians and pure physicians too)

Don't hide for ever behind their eingineering reasoning mathematicians since they do acquire those basically carpenter's skills of approximation to legalize their works

But you theoretical scientists don't have any true reasoning of any kind of approximation or alike to justify your earthy eingineering mathematics since truer and higher mathematics is universally must be valid and discovered

Calculus is also and in general an eingineering problem and never discovered mathematics

BKK

[Dan Christensen]

Post by bassam karzeddin
Relax Dan C. Troll since Zam's Lemma is also nonsese
Nobody can do anything meaningful in truly discovered mathematics munless (she/he) well-understand what is truly a real number fact

Let us understand what is and is not a truly a real number fact according to math failure BKK...


From Psycho Troll BKK who also wrote here:

“Those many challenges of mine (in my posts) weren't actually designed for human beings, but for the future artificial beings that would certainly replace them not far away from now, for sure.”
-- BKK, Dec. 6, 2017

“You know certainly that I'm the man, and more specially the KING who is going to upside down most of your current false mathematics for all future generations.”
-- BKK, Nov. 22, 2018

“Despite thousands of years of continuous juggling and false definitions of what is truly the real number, they [us carbon-based lifeforms?] truly don't want to understand it as was discovered strictly by the *KING* [BKK Himself!]”
-- BKK, Nov. 28, 2019

“I don't believe even in one being a number”
-- BKK, Dec. 31, 2019

Math failure, BKK, doesn't believe in negative numbers, zero, one or numbers like pi and root 2. He doesn't even believe in 40 degree angles or circles. Really! Needless to say his own goofy system is getting nowhere and never will. As such he is insanely jealous of wildly successful mainstream mathematics. He seems to believe these super-intelligent artificial beings of his will somehow be enlisting his aid to "reform" mathematics worldwide when they take over the planet in the near future. He is truly delusional.


Dan

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