This is for Dan-O-Matik who doesn't understand relational databases:

Just check out Relational Algebra:
https://en.wikipedia.org/wiki/Relational_algebra

Relations were somehow coinvented by Charles
Sanders Peirce and other Logicians to get out of
the limitations of Aristotelian Logic, so that we
have today First Order Logic based on Relations

aka Predicates. But Charles Sanders Peirce was
also funny guy, this might have been the locus where
Smullyan stole one of his Riddles:

"One of Peirce’s favorite examples helps elucidate the idea,
even if it perhaps be not perfectly politically correct:
Every Texan kills some Texan; no Texan is killed by
more than one Texan; therefore every Texan is killed
by some Texan. The argument’s conclusion follows
validly only if the set of Texans is finite."

Can you prove the above in DC Proof?

graham...@gmail.com schrieb am Dienstag, 24. März 2020 um 08:46:35 UTC+1:
> While working on PROLOG it occurred to me you only need 2 tables in a database
>
>
> TABLE binary
>
> < f1 f2 f3 f4 f5 f6 f7 f8 >
>
>
>
> TABLE ternary
>
> < f1 f2 f3 f4 f5 f6 f7 f8 >
>
>
> and 2 commands (from PROLOG)
>
> assert F1 F2
> remove F1 F2
>
>
> where F1 is a table name, and F2 is the INDEX.
>
> I used type VARCHAR on all fields
>
>
>
> www.TURBOPROLOG.com

"In 1870 Peirce published a long paper “Description of a Notation
for the Logic of Relatives” in which he introduced for the first time
in history, two years before Frege’s Begriffschrift a complete
syntax for the logic of relations of arbitrary adicity (or: arity)."
https://plato.stanford.edu/entries/peirce/

Mostowski Collapse schrieb am Sonntag, 30. Mai 2021 um 18:09:58 UTC+2:
> This is for Dan-O-Matik who doesn't understand relational databases:
>
> Just check out Relational Algebra:
> https://en.wikipedia.org/wiki/Relational_algebra
>
> Relations were somehow coinvented by Charles
> Sanders Peirce and other Logicians to get out of
> the limitations of Aristotelian Logic, so that we
> have today First Order Logic based on Relations
>
> aka Predicates. But Charles Sanders Peirce was
> also funny guy, this might have been the locus where
> Smullyan stole one of his Riddles:
>
> "One of Peirce’s favorite examples helps elucidate the idea,
> even if it perhaps be not perfectly politically correct:
> Every Texan kills some Texan; no Texan is killed by
> more than one Texan; therefore every Texan is killed
> by some Texan. The argument’s conclusion follows
> validly only if the set of Texans is finite."
>
> Can you prove the above in DC Proof?
> graham...@gmail.com schrieb am Dienstag, 24. März 2020 um 08:46:35 UTC+1:
> > While working on PROLOG it occurred to me you only need 2 tables in a database
> >
> >
> > TABLE binary
> >
> > < f1 f2 f3 f4 f5 f6 f7 f8 >
> >
> >
> >
> > TABLE ternary
> >
> > < f1 f2 f3 f4 f5 f6 f7 f8 >
> >
> >
> > and 2 commands (from PROLOG)
> >
> > assert F1 F2
> > remove F1 F2
> >
> >
> > where F1 is a table name, and F2 is the INDEX.
> >
> > I used type VARCHAR on all fields
> >
> >
> >
> > www.TURBOPROLOG.com

Ha Ha, Dan-O-Matik clueless in logic:

Clueless (1995): Trailer HQ
https://www.youtube.com/watch?v=3zuRkQSx5gs

Mostowski Collapse schrieb am Sonntag, 30. Mai 2021 um 18:16:09 UTC+2:
> "In 1870 Peirce published a long paper “Description of a Notation
> for the Logic of Relatives” in which he introduced for the first time
> in history, two years before Frege’s Begriffschrift a complete
> syntax for the logic of relations of arbitrary adicity (or: arity)."
> https://plato.stanford.edu/entries/peirce/
> Mostowski Collapse schrieb am Sonntag, 30. Mai 2021 um 18:09:58 UTC+2:
> > This is for Dan-O-Matik who doesn't understand relational databases:
> >
> > Just check out Relational Algebra:
> > https://en.wikipedia.org/wiki/Relational_algebra
> >
> > Relations were somehow coinvented by Charles
> > Sanders Peirce and other Logicians to get out of
> > the limitations of Aristotelian Logic, so that we
> > have today First Order Logic based on Relations
> >
> > aka Predicates. But Charles Sanders Peirce was
> > also funny guy, this might have been the locus where
> > Smullyan stole one of his Riddles:
> >
> > "One of Peirce’s favorite examples helps elucidate the idea,
> > even if it perhaps be not perfectly politically correct:
> > Every Texan kills some Texan; no Texan is killed by
> > more than one Texan; therefore every Texan is killed
> > by some Texan. The argument’s conclusion follows
> > validly only if the set of Texans is finite."
> >
> > Can you prove the above in DC Proof?
> > graham...@gmail.com schrieb am Dienstag, 24. März 2020 um 08:46:35 UTC+1:
> > > While working on PROLOG it occurred to me you only need 2 tables in a database
> > >
> > >
> > > TABLE binary
> > >
> > > < f1 f2 f3 f4 f5 f6 f7 f8 >
> > >
> > >
> > >
> > > TABLE ternary
> > >
> > > < f1 f2 f3 f4 f5 f6 f7 f8 >
> > >
> > >
> > > and 2 commands (from PROLOG)
> > >
> > > assert F1 F2
> > > remove F1 F2
> > >
> > >
> > > where F1 is a table name, and F2 is the INDEX.
> > >
> > > I used type VARCHAR on all fields
> > >
> > >
> > >
> > > www.TURBOPROLOG.com

On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> This is for Dan-O-Matik who doesn't understand relational databases:
>

I understand enough to know that you can only use a relational database to prove something about particular set of a data at some instant in time. You might be able to demonstrate some theorem of FOL, but you can't prove it in general.

Will consider your Texan puzzle. Looks like fun.

Dan

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

On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:

>
> "One of Peirce’s favorite examples helps elucidate the idea,
> even if it perhaps be not perfectly politically correct:
> Every Texan kills some Texan; no Texan is killed by
> more than one Texan; therefore every Texan is killed
> by some Texan. The argument’s conclusion follows
> validly only if the set of Texans is finite."
>
> Can you prove the above in DC Proof?

See http://dcproof.com/TexasPuzzle.htm

Dan

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

Now do it in set theory with FOL.
In FOL there is no step:

11 ALL(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
=> ALL(b):[b e t => EXIST(c):[c e t & f(c)=b]]]
Detach, 10, 6

12 ALL(b):[b e t => v(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [v(b)=v(c) => b=c]]
=> ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]
U Spec, 11

You cannot do ALL(f) inside a definition in FOL,
when f is a function symbol.

Dan Christensen schrieb am Sonntag, 30. Mai 2021 um 21:27:01 UTC+2:
> On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
>
> >
> > "One of Peirce’s favorite examples helps elucidate the idea,
> > even if it perhaps be not perfectly politically correct:
> > Every Texan kills some Texan; no Texan is killed by
> > more than one Texan; therefore every Texan is killed
> > by some Texan. The argument’s conclusion follows
> > validly only if the set of Texans is finite."
> >
> > Can you prove the above in DC Proof?
> See http://dcproof.com/TexasPuzzle.htm
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

I am not sure whether I can use your Finite definition
to provoke an inconsistency already. Have to think.
But if you allow ALL(f) there is no more guarantee

anymore that definitions are consistent. That a
definition axiom doesn't lead to an inconsistency.

Mostowski Collapse schrieb am Sonntag, 30. Mai 2021 um 23:50:18 UTC+2:
> Now do it in set theory with FOL.
> In FOL there is no step:
>
> 11 ALL(f):[ALL(b):[b e t => f(b) e t]
> & ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
> => ALL(b):[b e t => EXIST(c):[c e t & f(c)=b]]]
> Detach, 10, 6
>
> 12 ALL(b):[b e t => v(b) e t]
> & ALL(b):ALL(c):[b e t & c e t => [v(b)=v(c) => b=c]]
> => ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]
> U Spec, 11
>
> You cannot do ALL(f) inside a definition in FOL,
> when f is a function symbol.
> Dan Christensen schrieb am Sonntag, 30. Mai 2021 um 21:27:01 UTC+2:
> > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> >
> > >
> > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > even if it perhaps be not perfectly politically correct:
> > > Every Texan kills some Texan; no Texan is killed by
> > > more than one Texan; therefore every Texan is killed
> > > by some Texan. The argument’s conclusion follows
> > > validly only if the set of Texans is finite."
> > >
> > > Can you prove the above in DC Proof?
> > See http://dcproof.com/TexasPuzzle.htm
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, May 30, 2021 at 5:50:18 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 30. Mai 2021 um 21:27:01 UTC+2:
> > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> >
> > >
> > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > even if it perhaps be not perfectly politically correct:
> > > Every Texan kills some Texan; no Texan is killed by
> > > more than one Texan; therefore every Texan is killed
> > > by some Texan. The argument’s conclusion follows
> > > validly only if the set of Texans is finite."
> > >
> > > Can you prove the above in DC Proof?
> > See http://dcproof.com/TexasPuzzle.htm

> Now do it in set theory with FOL.

I think I will stick to the ordinary logic of most math textbooks.

> In FOL there is no step:
>
> 11 ALL(f):[ALL(b):[b e t => f(b) e t]
> & ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
> => ALL(b):[b e t => EXIST(c):[c e t & f(c)=b]]]
> Detach, 10, 6
>
> 12 ALL(b):[b e t => v(b) e t]
> & ALL(b):ALL(c):[b e t & c e t => [v(b)=v(c) => b=c]]
> => ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]
> U Spec, 11
>
> You cannot do ALL(f) inside a definition in FOL,
> when f is a function symbol.

There is no prohibition against quantifying over functions or sets in most math textbooks. Call it a variant of SOL if you like.

Dan

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

On Sunday, May 30, 2021 at 5:55:04 PM UTC-4, Mostowski Collapse wrote:
> I am not sure whether I can use your Finite definition
> to provoke an inconsistency already.

It's from Dedekind if that means anything you.

Dan

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

You can quantify over functions, if its set-like.

But for example this here:

ALL(b):[b e t => f(b) e t]

Doesn't make f set-like.

Dan Christensen schrieb am Montag, 31. Mai 2021 um 00:27:29 UTC+2:
> On Sunday, May 30, 2021 at 5:50:18 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Sonntag, 30. Mai 2021 um 21:27:01 UTC+2:
> > > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> > >
> > > >
> > > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > > even if it perhaps be not perfectly politically correct:
> > > > Every Texan kills some Texan; no Texan is killed by
> > > > more than one Texan; therefore every Texan is killed
> > > > by some Texan. The argument’s conclusion follows
> > > > validly only if the set of Texans is finite."
> > > >
> > > > Can you prove the above in DC Proof?
> > > See http://dcproof.com/TexasPuzzle.htm
> > Now do it in set theory with FOL.
> I think I will stick to the ordinary logic of most math textbooks.
> > In FOL there is no step:
> >
> > 11 ALL(f):[ALL(b):[b e t => f(b) e t]
> > & ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
> > => ALL(b):[b e t => EXIST(c):[c e t & f(c)=b]]]
> > Detach, 10, 6
> >
> > 12 ALL(b):[b e t => v(b) e t]
> > & ALL(b):ALL(c):[b e t & c e t => [v(b)=v(c) => b=c]]
> > => ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]
> > U Spec, 11
> >
> > You cannot do ALL(f) inside a definition in FOL,
> > when f is a function symbol.
> There is no prohibition against quantifying over functions or sets in most math textbooks. Call it a variant of SOL if you like.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, May 30, 2021 at 7:09:13 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 31. Mai 2021 um 00:27:29 UTC+2:
> > On Sunday, May 30, 2021 at 5:50:18 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Sonntag, 30. Mai 2021 um 21:27:01 UTC+2:
> > > > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> > > >
> > > > >
> > > > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > > > even if it perhaps be not perfectly politically correct:
> > > > > Every Texan kills some Texan; no Texan is killed by
> > > > > more than one Texan; therefore every Texan is killed
> > > > > by some Texan. The argument’s conclusion follows
> > > > > validly only if the set of Texans is finite."
> > > > >
> > > > > Can you prove the above in DC Proof?
> > > > See http://dcproof.com/TexasPuzzle.htm
> > > Now do it in set theory with FOL.
> > I think I will stick to the ordinary logic of most math textbooks.
> > > In FOL there is no step:
> > >
> > > 11 ALL(f):[ALL(b):[b e t => f(b) e t]
> > > & ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
> > > => ALL(b):[b e t => EXIST(c):[c e t & f(c)=b]]]
> > > Detach, 10, 6
> > >
> > > 12 ALL(b):[b e t => v(b) e t]
> > > & ALL(b):ALL(c):[b e t & c e t => [v(b)=v(c) => b=c]]
> > > => ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]
> > > U Spec, 11
> > >
> > > You cannot do ALL(f) inside a definition in FOL,
> > > when f is a function symbol.
> > There is no prohibition against quantifying over functions or sets in most math textbooks. Call it a variant of SOL if you like.
> > Dan

> You can quantify over functions, if its set-like.
>

I am aware of no such requirement in most math textbooks. Use these unnecessary restrictions if you must, e.g. in a philosophy course.

> But for example this here:
> ALL(b):[b e t => f(b) e t]
> Doesn't make f set-like.

Not a necessary or useful distinction AFAICT.

Dan

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

On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
>
> >
> > "One of Peirce’s favorite examples helps elucidate the idea,
> > even if it perhaps be not perfectly politically correct:
> > Every Texan kills some Texan; no Texan is killed by
> > more than one Texan; therefore every Texan is killed
> > by some Texan. The argument’s conclusion follows
> > validly only if the set of Texans is finite."
> >
> > Can you prove the above in DC Proof?
> See http://dcproof.com/TexasPuzzle.htm [deleted]

On further consideration, I will withdraw this proof. I assumed the functionality of the murderer/victim relation. While gang murders were ruled out, multiple murders by the same individual were not ruled.

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

On Monday, May 31, 2021 at 1:16:21 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
> > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> >
> > >
> > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > even if it perhaps be not perfectly politically correct:
> > > Every Texan kills some Texan; no Texan is killed by
> > > more than one Texan; therefore every Texan is killed
> > > by some Texan. The argument’s conclusion follows
> > > validly only if the set of Texans is finite."
> > >
> > > Can you prove the above in DC Proof?
> > See http://dcproof.com/TexasPuzzle.htm [deleted]
>
> On further consideration, I will withdraw this proof. I assumed the functionality of the murderer/victim relation. While gang murders were ruled out, multiple murders by the same individual were not ruled out.

Rule out such multiple murders and the conclusion would be easily shown to be correct.

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

On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
>
> >
> > "One of Peirce’s favorite examples helps elucidate the idea,
> > even if it perhaps be not perfectly politically correct:
> > Every Texan kills some Texan; no Texan is killed by
> > more than one Texan; therefore every Texan is killed
> > by some Texan. The argument’s conclusion follows
> > validly only if the set of Texans is finite."
> >
> > Can you prove the above in DC Proof?
> See http://dcproof.com/TexasPuzzle.htm [undeleted]

I will retract my retraction. By "Every Texan kills some Texan," Peirce probably did NOT mean AT LEAST ONE Texan. So, my proof stands. Sorry about the confusion.

> 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 presented the following explanation :
> On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
>> On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
>>
>>>
>>> "One of Peirce’s favorite examples helps elucidate the idea,
>>> even if it perhaps be not perfectly politically correct:
>>> Every Texan kills some Texan; no Texan is killed by
>>> more than one Texan; therefore every Texan is killed
>>> by some Texan. The argument’s conclusion follows
>>> validly only if the set of Texans is finite."
>>>
>>> Can you prove the above in DC Proof?
>> See http://dcproof.com/TexasPuzzle.htm [undeleted]
>
> I will retract my retraction. By "Every Texan kills some Texan," Peirce
> probably did NOT mean AT LEAST ONE Texan. So, my proof stands. Sorry about
> the confusion.

From T to T left total and right unique? Mass assisted suicide?

On Monday, May 31, 2021 at 5:56:58 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
> > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> >
> > >
> > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > even if it perhaps be not perfectly politically correct:
> > > Every Texan kills some Texan; no Texan is killed by
> > > more than one Texan; therefore every Texan is killed
> > > by some Texan. The argument’s conclusion follows
> > > validly only if the set of Texans is finite."
> > >
> > > Can you prove the above in DC Proof?
> > See http://dcproof.com/TexasPuzzle.htm [undeleted]
>
> I will retract my retraction. By "Every Texan kills some Texan," Peirce probably did NOT mean AT LEAST ONE Texan. So, my proof stands. Sorry about the confusion.

I have found that if you don't assume a unique victim for each "Texan", then the formal proof explodes in length from 16 to 507 in DC Proof.

I was able to prove:

ALL(x):ALL(k):[Set(x) & Set'(k)

& ALL(a):ALL(b):[(a,b) in k => a in x & b in x]

& ALL(a):[a in x => EXIST(b):[b in x & (a,b) in k]]

& ALL(a):ALL(b):ALL(c):[a in x & b in x & c in x => [(a,b) in k & (c,b) in k => a=c]]

=> [Finite(x) => ALL(a):[a in x => EXIST(b):(b,a) in k]]]

where

x is the set of Orks ("Texans" in the original)
(t, u) in k means t kills u

Dan

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

On Monday, May 31, 2021 at 5:56:58 PM UTC-4, Dan Christensen wrote:
> On Sunday, May 30, 2021 at 3:27:01 PM UTC-4, Dan Christensen wrote:
> > On Sunday, May 30, 2021 at 12:09:58 PM UTC-4, Mostowski Collapse wrote:
> >
> > >
> > > "One of Peirce’s favorite examples helps elucidate the idea,
> > > even if it perhaps be not perfectly politically correct:
> > > Every Texan kills some Texan; no Texan is killed by
> > > more than one Texan; therefore every Texan is killed
> > > by some Texan. The argument’s conclusion follows
> > > validly only if the set of Texans is finite."
> > >
> > > Can you prove the above in DC Proof?
> > See http://dcproof.com/TexasPuzzle.htm [undeleted]
>
> I will retract my retraction. By "Every Texan kills some Texan," Peirce probably did NOT mean AT LEAST ONE Texan. So, my proof stands. Sorry about the confusion.

I have found that if you don't assume a unique victim for each "Texan", then the formal proof explodes in length from 16 to 509 in DC Proof.

I was able to prove:

ALL(x):ALL(k):[Set(x) & Set'(k)

& ALL(a):ALL(b):[(a,b) in k => a in x & b in x]

& ALL(a):[a in x => EXIST(b):[b in x & (a,b) in k]]

& ALL(a):ALL(b):ALL(c):[a in x & b in x & c in x => [(a,b) in k & (c,b) in k => a=c]]

=> [Finite(x) => ALL(a):[a in x => EXIST(b):[b in x & (b,a) in k]]]

where

x is the set of Orks ("Texans" in the original)
(t, u) in k means t kills u

Dan

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