Come on guys, you can use Wolfgang Schwarz tree tool
any time. Just go to this URL: https://www.umsu.de/trees/

So Julio Di Egidio claimed:

Julio Di Egidio schrieb am Freitag, 1. September 2023 um 11:41:18 UTC+2:
> And it is in fact *reject*, since it's almost trivial
> that "forall P, P=t \/ P=f \/ P=something_else"
> implies "~ forall P, P=t \/ P=f".
https://groups.google.com/g/sci.logic/c/9qKL-CDn5Kg/m/HkaeI91bFwAJ

Is this true? Nope:

∀a(a=f ∨ (a=t ∨ a=m)) → ¬∀a(a=f ∨ a=t) is invalid.
https://www.umsu.de/trees/#~6a(a=f~2a=t~2a=m)~5~3~6a(a=f~2a=t)

Good Luck solving the Riddle!

SOI:SOI:SOI:SOI:SOI:SOI:SOI
...........___|___.........
....L..../.......[`\........
...LOL===........[__|.......
....L....\..........|.......
..........\_________/.......
............|...|...........
...........————————/........

Have Fun!

Hope you enjoy the ROFLcopter.

Mild Shock schrieb am Freitag, 1. September 2023 um 13:01:01 UTC+2:
> Come on guys, you can use Wolfgang Schwarz tree tool
> any time. Just go to this URL: https://www.umsu.de/trees/
>
> So Julio Di Egidio claimed:
>
> Julio Di Egidio schrieb am Freitag, 1. September 2023 um 11:41:18 UTC+2:
> > And it is in fact *reject*, since it's almost trivial
> > that "forall P, P=t \/ P=f \/ P=something_else"
> > implies "~ forall P, P=t \/ P=f".
> https://groups.google.com/g/sci.logic/c/9qKL-CDn5Kg/m/HkaeI91bFwAJ
>
> Is this true? Nope:
>
> ∀a(a=f ∨ (a=t ∨ a=m)) → ¬∀a(a=f ∨ a=t) is invalid.
> https://www.umsu.de/trees/#~6a(a=f~2a=t~2a=m)~5~3~6a(a=f~2a=t)

I don't think that this is the best kept secret of intutionistic
logic, but did nobody tell you guys, that a intuitionistically
valid formula, is also classically valid formula?

Here some useful acronyms:

IPC: Intuitionistic Propositional Calculus
CPC: Classical Propositional Calculus

Now there is this well known theorem:

|-_IPC φ implies |-_CPC φ

Now guess what would happen if IPC would not only reject
LEM, but also refute it, i.e. if we would also have:

|-_IPC ~LEM

We could then conclude that classical logic also refutes LEM:

|-_CPC ~LEM

But since classical logic accepts LEM, this would amount to
the claim that classical logic is inconsistent.

Mild Shock schrieb am Freitag, 1. September 2023 um 13:06:19 UTC+2:
> Good Luck solving the Riddle!
>
> SOI:SOI:SOI:SOI:SOI:SOI:SOI
> ..........___|___.........
> ...L..../.......[`\........
> ..LOL===........[__|.......
> ...L....\..........|.......
> .........\_________/.......
> ...........|...|...........
> ..........————————/........
>
> Have Fun!
>
> Hope you enjoy the ROFLcopter.
> Mild Shock schrieb am Freitag, 1. September 2023 um 13:01:01 UTC+2:
> > Come on guys, you can use Wolfgang Schwarz tree tool
> > any time. Just go to this URL: https://www.umsu.de/trees/
> >
> > So Julio Di Egidio claimed:
> >
> > Julio Di Egidio schrieb am Freitag, 1. September 2023 um 11:41:18 UTC+2:
> > > And it is in fact *reject*, since it's almost trivial
> > > that "forall P, P=t \/ P=f \/ P=something_else"
> > > implies "~ forall P, P=t \/ P=f".
> > https://groups.google.com/g/sci.logic/c/9qKL-CDn5Kg/m/HkaeI91bFwAJ
> >
> > Is this true? Nope:
> >
> > ∀a(a=f ∨ (a=t ∨ a=m)) → ¬∀a(a=f ∨ a=t) is invalid.
> > https://www.umsu.de/trees/#~6a(a=f~2a=t~2a=m)~5~3~6a(a=f~2a=t)