A Universal Quantifier - thoughts

Stream: maths

[Mr Proof]

I had some thoughts on type theory that I hope you don't mind if I share.

According to the Curry-Howard correspondence the quantifier $\Pi$ is related to the imply logic operator $\rightarrow$ and the $\Sigma$ quantifier is related to the $\land$ operator.

In Russel's logic he uses the Sheffer Stroke from which all other logic operations can be made. Hence we can form a quantifier which I'll write a $[A,x,B(x)]$ from which all other quantifiers can be made. Define $[A,B]=[A,\_,B]$ for the case where the types are not dependent then:
$A\rightarrow \bot =\overline{A} = [A,A]$
$A\times B = \overline{[A,B]}$
$A+B = [\overline{A},\overline{B}]$
$A\rightarrow B = [A,\overline{B}]$
$\prod_{x:A} B(x) = [A,x,\overline{B(x)}]$
$\sum_{x:A} B(x) = \overline{[A,x,B(x)]}$

The type theory axioms would be nearly the same with for example $\frac{\Gamma \vdash y:A, f:[A,x,B(x)] }{ f(y):\overline{B} }$

I think the difference between this and Lean is you can define the equivalent of "not" with the universal quantifier.

(a) What's your thoughts about how this would differ from the type theory in Lean? Would it need an extra axiom ("law of excluded middle"?) $[[A,A],[A,A]]\equiv A$
(b) How would you define this quantifier [A,x,B(x)] in Lean? (I think it would be equivalent to $(x:A)\rightarrow (B(x)\rightarrow \bot)$ or $\not\exists_{x:A} B(x)$ ). In other words I think all other quantifiers can be built from the "not-exists" quantifier

[Alex Meiburg]

One significant difference is that there's no clear computational interpretation of [A,B]. You could make this computable if you had an a computable version of LEM, [[A,A],[A,A]] = A -- but good luck with that!

[Kyle Miller]

Mr Proof said:

Σ is related to the imply logic operator → and the Π quantifier is related to the ∧ operator.

That should go the other way, pi types are related to implication and sigma types to conjunction.

[Mr Proof]

Alex Meiburg said:

One significant difference is that there's no clear computational interpretation of [A,B]. You could make this computable if you had an a computable version of LEM, [[A,A],[A,A]] = A -- but good luck with that!

I'm a bit of a novice at type theory. So what would "computable" mean in this sense. I think in language terms [A,B] would have to be interpreted as "the type (or proposition) A is incompatible with the type (or proposition) B".

[Giacomo Stevanato]

Mr Proof said:

Alex Meiburg said:

One significant difference is that there's no clear computational interpretation of [A,B]. You could make this computable if you had an a computable version of LEM, [[A,A],[A,A]] = A -- but good luck with that!

I'm a bit of a novice at type theory. So what would "computable" mean in this sense. I think in language terms [A,B] would have to be interpreted as "the type (or proposition) A is incompatible with the type (or proposition) B".

Also according to the Curry-Howard correspondence proofs can also be viewed as executable programs that create values of the types representing the proposition being proven. For example given a proof for a proposition like ∃ x, p x you would also be able to execute the proof to compute the value for the xthat actually satisfies p x. There are however some axioms that cannot be viewed as executable programs, most notably the Law of Excluded Middle (∀ p, p ∨ ¬p), because by using them you can materialize an instance of the type corresponding to a proposition without actually constructing one. See also intuitionistic/constructive logic.

[Edward van de Meent]

indeed. another famous axiom that cannot be viewed as an executable program is the axiom of choice (which implies the law of excluded middle)

[Mr Proof]

Do you think this analogy is correct: If I said it is impossible to build a proof system on the quantifier "not-exists" because that is impossible to prove. e.g. you can't prove unicorns don't exist. Just because you've never seen one doesn't mean they don't exist?

[Mario Carneiro]

Edward van de Meent said:

indeed. another famous axiom that cannot be viewed as an executable program is the axiom of choice (which implies the law of excluded middle)

Actually it can, there is an interpretation of double negation elimination in terms of call/cc and you can use that to prove LEM. It basically amounts to being able to explicitly manipulate the call stack, which can also be thought of as "going back in time".

Applied to the specific case of LEM, it is a program which, when asked "is p true or false?" returns "false" but also takes note of the current date. You can take this proof of ¬p (which is a function p -> False) and try to catch it in a lie if p happens to be true after all by constructing a proof of p and applying this function to it to get a proof of False, but the function that you were given instead rewinds time to the original query and returns "true" along with the proof of p you constructed.

[Patrick Stevens]

(There was some classic post about this, where you end up "covered in blood" or similar at the point where you've rewound and are handing on the proof of P. Anyone know which post I mean?)