Model Theory is used to confuse morons like Dan Christensen.
With Proof Theory we have already 4 outcomes.

Now with Model Theory, the |- gets a new buddy |=,
making things even more complicated, for squirel brains

like Dan Christensen. If we use the semantic definitions
of Antinomy and Tautology:

taut(φ) = ∀M (M |= φ)
ant(φ) = ∀M (M |= ~φ)

How is Antinomy the opposite of Tautology, we cannot prove:

taut(φ) <=> ~ant(φ)

For example the formula φ = P v Q is neither a Tautology nor an Antinomy.

How it started:
We gave Dan Christensen a definition of a new word "Antinomy",
a word he never did see or hear before in his entire life:

German:
"bezeichnet eine Aussagenfunktion, die unabhängig
von ihren Argumenten immer den Wert falsch ergibt"
https://de.wikipedia.org/wiki/Antilogie

English:
denotes a propositional function that always evaluates
to false, regardless of its arguments
https://de.wikipedia.org/wiki/Antilogie

How it is going:
First Dan Christensen renamed the word "Antinomy" from Model
Theory, into the word "Contradiction" from Proof Theory:
Dan Christensen schrieb am Sonntag, 27. August 2023 um 23:29:02 UTC+2:
> More usually, a contradiction.
https://groups.google.com/g/sci.logic/c/1AEjntgdDlk/m/nj_XB5X5FQAJ

Then Dan Christensen claimed the word "Contradictory", is
the opposite of the word "Tautology":
Dan Christensen schrieb am Montag, 28. August 2023 um 00:34:55 UTC+2:
> a contradiction is just the opposite of a tautology.
https://groups.google.com/g/sci.logic/c/1AEjntgdDlk/m/3Oe9iy39FQAJ

Woa! I have never seen more willful nonsense in written!

LMAO!

Mild Shock schrieb am Montag, 28. August 2023 um 09:21:14 UTC+2:
> Model Theory is used to confuse morons like Dan Christensen.
> With Proof Theory we have already 4 outcomes.
>
> Now with Model Theory, the |- gets a new buddy |=,
> making things even more complicated, for squirel brains
>
> like Dan Christensen. If we use the semantic definitions
> of Antinomy and Tautology:
>
> taut(φ) = ∀M (M |= φ)
> ant(φ) = ∀M (M |= ~φ)
>
> How is Antinomy the opposite of Tautology, we cannot prove:
>
> taut(φ) <=> ~ant(φ)
>
> For example the formula φ = P v Q is neither a Tautology nor an Antinomy.

On Monday, August 28, 2023 at 3:21:14 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

[snip childish abuse]

> like Dan Christensen. If we use the semantic definitions
> of Antinomy and Tautology:
>
> taut(φ) = ∀M (M |= φ)
> ant(φ) = ∀M (M |= ~φ)
>

Ha, ha! Mr. Collapse here can find no fault with my proposed resolution of the Liar Paradox: https://dcproof.com/LiarParadox2.htm

Once again he is reduced to quibbling about terminology as if it made any difference. What else could he do, I suppose?

Dan

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

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

A counter example to your claim is for example the formula
P v Q. You can use an easy tool, namely the Stanford
Truth table generator to see that:

P Q (P ∨ Q)
F F F
F T T
T F T
T T T
https://web.stanford.edu/class/cs103/tools/truth-table-tool/

Its neither a Tautology, not all rows are "T". Its neither
an Antinomy, not all rows are "F". So its not an opposite
pair like Odd and Even.

We don't have natural numbers that are neither Odd nor
Even. But we have formulas that are neither Antinomies
nor Tautologies. So the later two are not strictly opposite.

Dan Christensen schrieb am Montag, 28. August 2023 um 18:18:43 UTC+2:
> On Monday, August 28, 2023 at 3:21:14 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
>
> [snip childish abuse]
> > like Dan Christensen. If we use the semantic definitions
> > of Antinomy and Tautology:
> >
> > taut(φ) = ∀M (M |= φ)
> > ant(φ) = ∀M (M |= ~φ)
> >
> Ha, ha! Mr. Collapse here can find no fault with my proposed resolution of the Liar Paradox: https://dcproof.com/LiarParadox2.htm
>
> Once again he is reduced to quibbling about terminology as if it made any difference. What else could he do, I suppose?
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

What you did, you rejected LEM, this classical law:

In logic, the law of excluded middle (or the principle of excluded middle)
states that for every proposition, either this proposition or its negation is true.
https://en.wikipedia.org/wiki/Law_of_excluded_middle

Because in your Trichotomy you cannot prove:

b e f | b e t

But the Liar Antinomy is classically equivalent to LEM. You
can use negation normal form rules, to see that the Liar Antinomy
is classically equivalent to LEM:

A <=> ~~> (A => B) & (B => A)
A => B ~~> ~A | B
~(A | B) ~~> ~A & ~B
~(A & B) ~~> ~A | ~B
~~A ~~> A
https://en.wikipedia.org/wiki/Negation_normal_form

Negation normal form is in many ways a classical operation,
since it has not only double negation elimination ~~A ~~> A,
but also implication is bootstrapped A => B ~~> ~A | B, making

it material implication and not strict implication. Here is the
negation normal form of the Liar Antinomy, it gives me
LEM in a few steps:

~(p <=> ~p) ~~>
~((p => ~p) & (~p => p) ~~>
~((~p | ~p) & (~~p | p)) ~~>
~((~p | ~p) & (p | p)) ~~>
~(~p & p) ~~>
~~p | ~p ~~>
p | ~p

So in classical logic the Liar Antinomy is indeed equivalent to LEM.

Mild Shock schrieb am Montag, 28. August 2023 um 18:38:34 UTC+2:
> A counter example to your claim is for example the formula
> P v Q. You can use an easy tool, namely the Stanford
> Truth table generator to see that:
>
> P Q (P ∨ Q)
> F F F
> F T T
> T F T
> T T T
> https://web.stanford.edu/class/cs103/tools/truth-table-tool/
>
> Its neither a Tautology, not all rows are "T". Its neither
> an Antinomy, not all rows are "F". So its not an opposite
> pair like Odd and Even.
>
> We don't have natural numbers that are neither Odd nor
> Even. But we have formulas that are neither Antinomies
> nor Tautologies. So the later two are not strictly opposite.
> Dan Christensen schrieb am Montag, 28. August 2023 um 18:18:43 UTC+2:
> > On Monday, August 28, 2023 at 3:21:14 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> >
> > [snip childish abuse]
> > > like Dan Christensen. If we use the semantic definitions
> > > of Antinomy and Tautology:
> > >
> > > taut(φ) = ∀M (M |= φ)
> > > ant(φ) = ∀M (M |= ~φ)
> > >
> > Ha, ha! Mr. Collapse here can find no fault with my proposed resolution of the Liar Paradox: https://dcproof.com/LiarParadox2.htm
> >
> > Once again he is reduced to quibbling about terminology as if it made any difference. What else could he do, I suppose?
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Relative to a two valued model M, every sentence
should have either M |= b or ~M |= b. The forcing
relationship |= decides every sentence inside a model.

This is the form of LEM that spuns from model theory.
If we interpret b e t as M |= b in some hidden model M
and b e f as ~M |= b in the same hidden model M,

then we should have b e t or b e f. You can define the
sets f and t, for some model M, as follows:

f = { b e s | M |= s }
t = { b e s | ~M |= s }

They obviously form a bi-partition of the set s, and hence
LEM should be satisfied. You need a new model theory
to understand your multivalued logic Liar, the usual binary

model theory doesn't work anymore, since what would be:

m = ??

Mild Shock schrieb am Mittwoch, 30. August 2023 um 09:03:46 UTC+2:
> What you did, you rejected LEM, this classical law:
>
> In logic, the law of excluded middle (or the principle of excluded middle)
> states that for every proposition, either this proposition or its negation is true.
> https://en.wikipedia.org/wiki/Law_of_excluded_middle
>
> Because in your Trichotomy you cannot prove:
>
> b e f | b e t
>
> But the Liar Antinomy is classically equivalent to LEM. You
> can use negation normal form rules, to see that the Liar Antinomy
> is classically equivalent to LEM:
>
> A <=> ~~> (A => B) & (B => A)
> A => B ~~> ~A | B
> ~(A | B) ~~> ~A & ~B
> ~(A & B) ~~> ~A | ~B
> ~~A ~~> A
> https://en.wikipedia.org/wiki/Negation_normal_form
>
> Negation normal form is in many ways a classical operation,
> since it has not only double negation elimination ~~A ~~> A,
> but also implication is bootstrapped A => B ~~> ~A | B, making
>
> it material implication and not strict implication. Here is the
> negation normal form of the Liar Antinomy, it gives me
> LEM in a few steps:
>
> ~(p <=> ~p) ~~>
> ~((p => ~p) & (~p => p) ~~>
> ~((~p | ~p) & (~~p | p)) ~~>
> ~((~p | ~p) & (p | p)) ~~>
> ~(~p & p) ~~>
> ~~p | ~p ~~>
> p | ~p
>
> So in classical logic the Liar Antinomy is indeed equivalent to LEM.
> Mild Shock schrieb am Montag, 28. August 2023 um 18:38:34 UTC+2:
> > A counter example to your claim is for example the formula
> > P v Q. You can use an easy tool, namely the Stanford
> > Truth table generator to see that:
> >
> > P Q (P ∨ Q)
> > F F F
> > F T T
> > T F T
> > T T T
> > https://web.stanford.edu/class/cs103/tools/truth-table-tool/
> >
> > Its neither a Tautology, not all rows are "T". Its neither
> > an Antinomy, not all rows are "F". So its not an opposite
> > pair like Odd and Even.
> >
> > We don't have natural numbers that are neither Odd nor
> > Even. But we have formulas that are neither Antinomies
> > nor Tautologies. So the later two are not strictly opposite.
> > Dan Christensen schrieb am Montag, 28. August 2023 um 18:18:43 UTC+2:
> > > On Monday, August 28, 2023 at 3:21:14 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > >
> > > [snip childish abuse]
> > > > like Dan Christensen. If we use the semantic definitions
> > > > of Antinomy and Tautology:
> > > >
> > > > taut(φ) = ∀M (M |= φ)
> > > > ant(φ) = ∀M (M |= ~φ)
> > > >
> > > Ha, ha! Mr. Collapse here can find no fault with my proposed resolution of the Liar Paradox: https://dcproof.com/LiarParadox2.htm
> > >
> > > Once again he is reduced to quibbling about terminology as if it made any difference. What else could he do, I suppose?
> > >
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com
> > > 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 build a theorem prover, based on the idea of
the two sets f and t. You would just express what M |= A
does to the different connectives that make up a propositional

formula A, and you can use it to search for models. Example
rules that work for the connectives (/\)/2, (\/)/2 and (~)/1:

Alpha Rules:
A /\ B e T ~~> A e T, B e T
A \/ B e F ~~> A e F, B e F

Beta Rules:
A /\ B e F ~~> A e F; B e F
A \/ B e T ~~> A e T; B e T

Other rules:
~A e F ~~> A e T
~A e T ~~> A e F

Beta rules need backtracking, since they fork the tableaux
search. Alpha rules are straight way reductions, that create
more formulas in a branch.

See also:
https://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Propositional_tableau_with_unification

Jens Ottens leanCop performs the rules in advance through
negation normal form, and then only performs the model
search through backtracking.

Mild Shock schrieb am Donnerstag, 31. August 2023 um 09:32:52 UTC+2:
> Relative to a two valued model M, every sentence
> should have either M |= b or ~M |= b. The forcing
> relationship |= decides every sentence inside a model.
>
> This is the form of LEM that spuns from model theory.
> If we interpret b e t as M |= b in some hidden model M
> and b e f as ~M |= b in the same hidden model M,
>
> then we should have b e t or b e f. You can define the
> sets f and t, for some model M, as follows:
>
> f = { b e s | M |= s }
> t = { b e s | ~M |= s }
>
> They obviously form a bi-partition of the set s, and hence
> LEM should be satisfied. You need a new model theory
> to understand your multivalued logic Liar, the usual binary
>
> model theory doesn't work anymore, since what would be:
>
> m = ??
> Mild Shock schrieb am Mittwoch, 30. August 2023 um 09:03:46 UTC+2:
> > What you did, you rejected LEM, this classical law:
> >
> > In logic, the law of excluded middle (or the principle of excluded middle)
> > states that for every proposition, either this proposition or its negation is true.
> > https://en.wikipedia.org/wiki/Law_of_excluded_middle
> >
> > Because in your Trichotomy you cannot prove:
> >
> > b e f | b e t
> >
> > But the Liar Antinomy is classically equivalent to LEM. You
> > can use negation normal form rules, to see that the Liar Antinomy
> > is classically equivalent to LEM:
> >
> > A <=> ~~> (A => B) & (B => A)
> > A => B ~~> ~A | B
> > ~(A | B) ~~> ~A & ~B
> > ~(A & B) ~~> ~A | ~B
> > ~~A ~~> A
> > https://en.wikipedia.org/wiki/Negation_normal_form
> >
> > Negation normal form is in many ways a classical operation,
> > since it has not only double negation elimination ~~A ~~> A,
> > but also implication is bootstrapped A => B ~~> ~A | B, making
> >
> > it material implication and not strict implication. Here is the
> > negation normal form of the Liar Antinomy, it gives me
> > LEM in a few steps:
> >
> > ~(p <=> ~p) ~~>
> > ~((p => ~p) & (~p => p) ~~>
> > ~((~p | ~p) & (~~p | p)) ~~>
> > ~((~p | ~p) & (p | p)) ~~>
> > ~(~p & p) ~~>
> > ~~p | ~p ~~>
> > p | ~p
> >
> > So in classical logic the Liar Antinomy is indeed equivalent to LEM.
> > Mild Shock schrieb am Montag, 28. August 2023 um 18:38:34 UTC+2:
> > > A counter example to your claim is for example the formula
> > > P v Q. You can use an easy tool, namely the Stanford
> > > Truth table generator to see that:
> > >
> > > P Q (P ∨ Q)
> > > F F F
> > > F T T
> > > T F T
> > > T T T
> > > https://web.stanford.edu/class/cs103/tools/truth-table-tool/
> > >
> > > Its neither a Tautology, not all rows are "T". Its neither
> > > an Antinomy, not all rows are "F". So its not an opposite
> > > pair like Odd and Even.
> > >
> > > We don't have natural numbers that are neither Odd nor
> > > Even. But we have formulas that are neither Antinomies
> > > nor Tautologies. So the later two are not strictly opposite.
> > > Dan Christensen schrieb am Montag, 28. August 2023 um 18:18:43 UTC+2:
> > > > On Monday, August 28, 2023 at 3:21:14 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > > >
> > > > [snip childish abuse]
> > > > > like Dan Christensen. If we use the semantic definitions
> > > > > of Antinomy and Tautology:
> > > > >
> > > > > taut(φ) = ∀M (M |= φ)
> > > > > ant(φ) = ∀M (M |= ~φ)
> > > > >
> > > > Ha, ha! Mr. Collapse here can find no fault with my proposed resolution of the Liar Paradox: https://dcproof.com/LiarParadox2.htm
> > > >
> > > > Once again he is reduced to quibbling about terminology as if it made any difference. What else could he do, I suppose?
> > > >
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com