EXMID <-> ~P 1o e. Fin

[jkingdon]

It seems very likely that EXMID <-> ~P 1o e. Fin can be proved in light of EXMID ↔ 𝒫 1o = 2o , 𝒫 1o ≠ 3o, 𝒫 1o ≠ 1o, etc.

[icecream17]

(~P 1o e. Fin seems to imply EXMID thanks to https://us.metamath.org/ileuni/fidceq.html and the other direction is true so it is indeed provable)

[benjub]

... is true so it is indeed provable

Like the consistency of ZF ? ;)

[benjub]

We can easily prove EXMID <-> ~P 1o C_ Fin, but I am not sure about ~P 1o e. Fin -> EXMID, since there may be some models of set theory over many-valued logics ?

[icecream17]

fidceq
((~P 1o ∈ Fin ∧ x ∈ ~P 1o ∧ 1o ∈ ~P 1o) → DECID x = 1o)

existence, pwid, mp3an3
((~P 1o ∈ Fin ∧ x ∈ ~P 1o) → DECID x = 1o)

existence, elpw, sylan2br
((~P 1o ∈ Fin ∧ x C_ 1o) → DECID x = 1o)

equalities (df1o2)
((~P 1o ∈ Fin ∧ x C_ {(/)}) → DECID x = {(/)})

exmid1dc
(~P 1o ∈ Fin → EXMID)

[jkingdon]

We can easily prove EXMID <-> ~P 1o C_ Fin, but I am not sure about ~P 1o e. Fin -> EXMID, since there may be some models of set theory over many-valued logics ?

Many-valued logic like there is a truth value which isn't either true or false? To be honest I don't know which axioms we'd need to change to get that kind of logic, but that isn't possible in the logic we have - see https://us.metamath.org/ileuni/pwtrufal.html and section 1.1 of [Bauer] which discusses this topic explicitly.

[jkingdon]

... is true so it is indeed provable

Like the consistency of ZF ? ;)

LOL I can see I'm not the only one who sees something like "x is true" and has at least a momentary mental bump as I process what is really being said.

[benjub]

Many-valued logic like there is a truth value which isn't either true or false? To be honest I don't know which axioms we'd need to change to get that kind of logic, but that isn't possible in the logic we have - see https://us.metamath.org/ileuni/pwtrufal.html and section 1.1 of [Bauer] which discusses this topic explicitly.

First, @icecream17's proof shows that what I had in mind doesn't exactly work, but related ideas may still be worth some investigations. This is not defeated by pwtrufal or Section 1.1 in Bauer's "Fives Stages" in that I do not want to prove that there are other truth values than True or False: I only want, by providing a model which has such truth values, to show that we cannot exclude it. (In the same way that classical logic is not excluded by (neutral) intuitionistic logic: it is simply not imposed.)

My idea was based on the fact that $\mathcal{P}(1)$ can be thought of as the set of truth values, and then to use some of the many-valued logics: for an $n$-valued logic with $2 < n < \infty$, we would have finiteness of $\mathcal{P}(1)$ but no excluded middle. So my idea was to construct a set theory (at least, enough of a set theory) based on one of these logics. By the above proof, this is doomed, but I'd like to pinpoint where.

[digama0]

n-valued logic is not intuitionistic. You will have to break one of the other axioms of propositional logic to implement n-valued logic. If you did so, I don't think the rest of set theory would be particularly broken, and you may be able to have an axiom saying there are 5 truth values or something, but intuitionistic logic definitely proves that there cannot be 3 or 4 or 5 truth values. The only possible value is 2, and pwtrufal basically tells you this.

[jkingdon]

n-valued logic is not intuitionistic. You will have to break one of the other axioms of propositional logic to implement n-valued logic. If you did so, I don't think the rest of set theory would be particularly broken, and you may be able to have an axiom saying there are 5 truth values or something, but intuitionistic logic definitely proves that there cannot be 3 or 4 or 5 truth values. The only possible value is 2, and pwtrufal basically tells you this.

Another result which expresses this is https://us.metamath.org/ileuni/pwntru.html in case that is more clear.

[benjub]

Ah, thanks ! So Jim was right to point me to pwtrufal, and now I understand better. I'm going to look a bit more at what $\mathcal{P}(1)$ can be in various models of intuitionistic logic, in particular in topos theoretic models. It's proved in https://us.metamath.org/ileuni/pw1on.html that it is an ordinal, but without excluded middle, ordinals can be pretty wild...

[jkingdon]

without excluded middle, ordinals can be pretty wild...

The kind of ordinals currently defined in iset.mm (recursively transitive sets) are also called Powell ordinals. There are at least two other commonly used definitions (probably more, I'm only dimly aware of this stuff). I suppose one place to start on this is https://mathoverflow.net/questions/452678/does-negative-trichotomy-hold-for-constructive-ordinals especially the comment "In constructive settings, there really aren’t enough such orderings, and this motivates the zoo of other notions of ordinals, whose relationships are rather subtler." (read that in context for a definition of "such orderings").