Reputation
Top tag
Next privilege 250 Rep.
View close votes
Badges
9
Newest
 Curious
Impact
~2k people reached

  • 0 posts edited
  • 0 helpful flags
  • 8 votes cast
Dec
2
comment Are there non-trival logics that exibit soundness and completeness that are not first order?
That's pretty much the answer I'm looking for
Dec
2
asked Are there non-trival logics that exibit soundness and completeness that are not first order?
Jul
2
awarded  Curious
Dec
26
accepted Give an example of a program in Simply Typed Lambda that produces Bottom.
Sep
30
revised Give an example of a program in Simply Typed Lambda that produces Bottom.
more words
Sep
30
comment Give an example of a program in Simply Typed Lambda that produces Bottom.
@Trismegistos is right, simply typed lambda calculus is apparently equivalent to minimal logic. minimal logic has the ability to make statements in the form A→⊥, thus there should be a way to introduce ⊥, and construct a lambda function with the signature A→⊥ iff A is empty. Or I'm misunderstanding something else.
Sep
30
comment Give an example of a program in Simply Typed Lambda that produces Bottom.
This is not homework. I've been trying to learn type theory on my own time.
Sep
30
asked Give an example of a program in Simply Typed Lambda that produces Bottom.
Sep
28
comment What can be proven within Simply Typed lambda calculus?
So is the computation component essentially pointless? Minimal logic doesn't seem that useful either.
Sep
27
awarded  Editor
Sep
27
revised What can be proven within Simply Typed lambda calculus?
I copied the wrong link :-(
Sep
26
comment What can be proven within Simply Typed lambda calculus?
Yes. Sorry for the ambiguity.
Sep
26
asked What can be proven within Simply Typed lambda calculus?
Jul
31
answered Peano axioms expressed in type theory
Apr
4
awarded  Commentator
Apr
4
comment How to start with automated theorem proving?
@Q__ If you try this and run into any issues let me know!
Apr
3
accepted Peano axioms expressed in type theory
Apr
3
comment Peano axioms expressed in type theory
Here is what was throwing me off math.stackexchange.com/questions/350145/… . Thanks again for your posts!
Apr
3
asked Variables in Types in type theory
Apr
3
comment Peano axioms expressed in type theory
I'll break my confusion into a separate question. Mostly I'm confused because in the formulations of type theory I'm reading there is nothing justifying variable (or quantification) in the types themselves. Thanks for your answers!