2

I have a problem reading existing question's answers. I've successfully encoded the proof of one of De Morgan's Laws, ¬∃x P(x) → ∀x ¬P(x), for Quantifiers formally via cubicaltt type-checker via Curry-Howard correspondence, the solution is available on GitHub. As the basis, I took the answers from StackExchange question mentioned above, but as I went through their steps, this was unclear to me:

All the answers are using a strange (for a person who isn't too familiar with formal logic) notion of mentioning a predicate without a quantifier, and then using rules like ∀-intro and ∃-intro. For example, the first, accepted answer assumes P(x) in its second step. What would be a Curry-Howard counterpart to something like that? What is the meaning of P(x) and how is it different from ∀xP(x)?

It uses ∃-intro in one step, and ∀-intro in another (step 6). Obviously, you cannot just arbitrary add ∃ or ∀ whenever you want. What are the rules, and which is permitted to use and when?

Kostiantyn Rybnikov
  • 133
  • 4
  • 1
    I think `P(x)`might be a typo and what is meant is `P(a)` where `a` is an arbitrary constant (note the `[a]` in that line). `P(a)` doesn't need a quantifier since `a` is not a variable. Similarly line 5 should be `~P(a)`. Does this clarify anything for you? – E... Feb 07 '19 at 23:08

1 Answers1

1

It uses ∃-intro in one step, and ∀-intro in another (step 6). Obviously, you cannot just arbitrary add ∃ or ∀ whenever you want. What are the rules, and which is permitted to use and when?

You can introduce an existential when you've established the existence of a witness.

You can introduce an universal only when you are handling an arbitrary assumed term (does not occur free in any statement referred from outside the scope of this assumption).

Now, as in the answer in question, some proof writers/checkers just introduce a new free variable without fanfare, or reuse the quantified term. I prefer to explicitly raise an assumption, declaring the term used in the scope of the subproof. I also encourage using indenting to track scopes of assumptions as they are raised and discharged.

1.|_ ¬∃x P(x) --- premise
2.|  |_ [c] --- assumed ... with the requirement that c does not occur free in the premise
3.|  |  |_ P(c) --- assumed
4.|  |  |  ∃x P(x) --- from 3) by ∃-intro ... true under the assumption that a witness does exist
5.|  |  |  ⊥ --- contradiction, from 1) and 4)
6.|  |  ¬P(c) --- from 3) to 5) by ¬-intro 
7.|  ∀x ¬P(x) --- from 6) by ∀-intro ... under the guarantee that c was arbitrary
Graham Kemp
  • 2,346
  • 7
  • 13