search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Add decidability connective to iset.mm #362

Closed jkingdon closed 6 years ago

jkingdon commented 6 years ago

As discussed in some comments on #350 it would be good to have a notation for decidability. This can be used as an antecedent or a hypothesis (which probably will be a more graceful way to display classical results than to try to keep track of what does and does not depend on ax-3).

Decidability can also be used as a conclusion (if a formula implies the decidability of an arbitrary proposition, then that formula cannot be a theorem of intuitionistic logic).

My work in progress is here: https://github.com/metamath/set.mm/compare/develop...jkingdon:decidability-connective?expand=1 but before I make that into a pull request, I would like comments on:

  1. Notation. One option at https://github.com/metamath/set.mm/issues/350#issuecomment-372088793 was LEM ph but that strikes me as confusing, since the Law of the Excluded Middle (LEM) is generally taken to be the assertion that all propositions are decidable, rather than being about decidability of a particular proposition. I also considered DECIDABLE ph but my current branch has DECID ph which I was thinking is a compromise between the explicitness of DECIDABLE ph and something even more concise (I'm a little cool on something very concise, given that there isn't a standard notation for this that I know of, short of ph is decidable in words).

  2. Anything about the syntax or semantics of this definition. It seems straightforward (with the syntax being very much like -. and the semantics being, well, just like ph \/ -. ph). But I won't claim to be any flavor of expert.

  3. Typesetting. Right now it typesets with small caps DECID next to the formula and spacing similar to ¬ (so DECID x = y is typeset similarly to ¬ x = y). Coming up with something which people find readable is relevant to whether this is a good notation.

  4. Anything else?

digama0 commented 6 years ago

I'm not particularly invested in the name, and am fine with DECID ph. But since it was my suggestion, as a justification of LEM ph, I would argue it by analogy to AC(X) notation for parameterized AC. The idea is that LEM(ph) is a weak form of LEM relativized to a single proposition, and LEM(ph) for all ph is the actual axiom of excluded middle. Maybe it is easier to use just EM ph, which can be read as "ph has excluded middle", which I think correctly conveys the sense in which this is like LEM but particularized to ph.

By the way, this partially comes back to that axiom we discussed before, which can in this notation be written DECID A. x x = y, which expresses that the space of object variables (not the universe that those variables range over, the variables themselves, generally taken to be indexed by natural numbers in the metatheory) has decidable equality. This allows for a lot of set.mm's reasoning by cases on distinctors.

Then again, I now think that it is better to assert the non-exclusive disjunction A. x x = y \/ NF_ x y (strictly non-exclusive only when the universe has one element), because the first statement has some possibly undesirable decidability statements equivalent to DECID(the universe has one element) in the absence of dtru.

jkingdon commented 6 years ago

I'm moving the decidable distinctness discussion to #364

jkingdon commented 6 years ago

Yeah, I see how "p is decidable" can be seen as a sort of parameterized LEM just as "x has a choice function" can be seen as a parameterized Axiom of Choice. But I still prefer something which is a slightly more direct notational equivalent to "p is decidable" (that being a less unwieldy phrase than "x has a choice function" works in our favor).

I've submitted my work so far as pull request #365 and that could be merged, unless people want more discussion.