Talk:Higher-order logic

This is the talk page for discussing improvements to the Higher-order logic article.
This is not a forum for general discussion of the article's subject.

Put new text under old text. Click here to start a new topic.
New to Wikipedia? Welcome! Learn to edit; get help.

Article policies

Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL

Mathematics Mid‑priority

	Mathematics portal 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.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
Mid	This article has been rated as Mid-priority on the project's priority scale.

Philosophy: Logic High‑importance

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.PhilosophyWikipedia:WikiProject PhilosophyTemplate:WikiProject PhilosophyPhilosophy articles

High

This article has been rated as High-importance on the project's importance scale.

Associated task forces:
/
	Logic

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. 24.95.48.112 01:53, 7 March 2007 (UTC)[reply]

- 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 203.169.23.13 (talk) 22:10, 23 May 2008 (UTC)[reply]

- 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 195.72.96.179 (talk) 13:08, 29 September 2008 (UTC)[reply]

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 83.23.16.6 (talk) 19:53, 6 May 2012 (UTC)[reply]

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

ruin[edit]

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

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. 86.127.138.67 (talk) 23:50, 15 April 2015 (UTC)[reply]

Basics are definitely needed. While it's easy to find sources and examples for the elementary "in first order logic, you can quantify only over individuals, whereas in second order logic, you can also quantify over predicates", it's not immediately clear how those generalise to third and higher orders; this article should answer that question. The few hints given on how the hierarchy is built up (i.e., on how order is counted) focus on the semantics — what types of objects would show up in an interpretation of the logic — but isn't it an important point of higher-order logic that the restrictions imposed (or relative to first-order logic: not imposed) are purely syntactic? Expert attention might also be needed to the question of whether the definition of (say) third-order logic is agreed upon in the literature, or contradictory definitions are used; I see a different risk that there could be different choices on how to count order. 130.243.68.247 (talk) 14:19, 7 December 2018 (UTC)[reply]

This article is a lot clearer and better-organised than the one on First-order logic: one could be forgiven for thinking that this article were addressing the more basic, beginner level, so comparatively elegant and simple it is.

Nuttyskin (talk) 10:04, 31 March 2023 (UTC)[reply]

behavioral manding[edit]

this page is watered down and wrung like a tree. if you ever want society to get better without you being at fault don't pull your punches by decentralizing the critical aspects of replicating the topic. HexClock (talk) 21:28, 20 May 2023 (UTC)[reply]

Higher-order functions[edit]

This article doesn't mention higher order functions. Are higher-order functions included in higher-order logic? Jarble (talk) 21:51, 5 December 2023 (UTC)[reply]