Talk:Higher-order logic

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Mathematics (Rated Start-class, Mid-priority)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
Start Class
Mid Priority
 Field: Foundations, logic, and set theory
WikiProject Philosophy (Rated Start-class, High-importance)
WikiProject icon This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 High  This article has been rated as High-importance on the project's importance scale.

Another definition is that functions can not be passed as arguments in lower-order logic.

Sure they can. \P\Q\x(R(P) ^ Q(x)). I guess that's actually lambda calc, but it's certainly not HOL. 01:53, 7 March 2007 (UTC)

- This sentence is vague to the point of comical "in first-order logic, roughly speaking, it is forbidden to quantify over predicates." Are we 'roughly speaking' or are we speaking of 'logic'?...we can't have both. i.e. Either 'first order logic' supports quantification over predicates, or it doesn't. Which is it? —Preceding unsigned comment added by (talk) 22:10, 23 May 2008 (UTC)

- I, think it would be more intuitive to compare higher order logic to second order logic instead of first order logic. —Preceding unsigned comment added by (talk) 13:08, 29 September 2008 (UTC)

Set of all statements[edit]

Can we consider set of all HOL statements as set of ALL statements? I know it may be not set in traditional sense, possibly rather class of statements, but I think you know what I mean (talk) 19:53, 6 May 2012 (UTC)

What do you think will be the cardinality of this set? Poshida (talk) 06:54, 17 September 2015 (UTC)


you people are ruining true mathematics, coming up with rules to satisfy sociology (talk) 10:05, 28 October 2013 (UTC)

some basics needed[edit]

This article gets too quickly to talk of type theory and related results. It needs a basic introduction/definitions to why type are needed in HOL. And hand-in-hand with that it should explain the two constructions of classical HOL: one with comprehension axioms and the other with lambda-abstractions. For the latter I can suggest the introductory pages to Melvin Fitting's book Types, Tableaux, and Gödel's God; although the book is mostly about modal HOL, it does have a good intro to classical HOL. (talk) 23:50, 15 April 2015 (UTC)