Timeline for Propositional Logic, First-Order Logic, and Higher-Order Logics
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 5, 2011 at 15:32 | comment | added | Mark Adams | b) I'm not particularly familiar with semantics, but as I understand it semantics deals with values, or at least equivalences between values. The type system of a formal language would partition values in the semantics, forbidding equivalences between values of different type. | |
| Feb 5, 2011 at 15:26 | comment | added | Mark Adams | a) In higher-order logic, variables can range over any values. In nth-order logic there is explicit distinction between different kinds of variable, which must range over (n-1)th order values or lower. So in a logic dealing with natural numbers, a 0th-order value would be a natural number, a 1st-order value would be a function over natural numbers, e.g "+", a 2nd-order value is a function that takes function arguments, e.g. "IsBijection", etc. Higher-order logic does not necessarily imply use of type theory/category theory. | |
| Feb 5, 2011 at 15:10 | comment | added | Mark Adams | @Noldorin: I forgot to say in the answer to (4) that there are 1st-order logics that are not as powerful as natural number arithmetic and so the Incompleteness Theorem says nothing about these. But 1st-order logic with natural numbers is necessarily incomplete. | |
| Jan 31, 2011 at 17:19 | comment | added | Noldorin | @Mark: Thanks for your response. This is a great answer; it answers many of my questions without being needlessly technical. Just a couple of little clarifications really: a) how exactly do nth-order logic and higher-order logic differ? (I always understood them to be the same thing.) does higher-order logic imply the use of type theory/category theory? b) How does a formal logic with a type theory relate to its semantics? They seem closely related, but I can't say much more. | |
| Jan 30, 2011 at 20:26 | history | edited | Mark Adams | CC BY-SA 2.5 |
inserted missing words
|
| Jan 29, 2011 at 10:18 | history | edited | Mark Adams | CC BY-SA 2.5 |
filled in missing word
|
| Jan 29, 2011 at 8:49 | history | edited | Mark Adams | CC BY-SA 2.5 |
corrected grammatic error
|
| Jan 29, 2011 at 8:43 | history | answered | Mark Adams | CC BY-SA 2.5 |