Questions tagged [higher-order-logic]

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. (Def: http://en.m.wikipedia.org/wiki/Higher-order_logic)

Filter by
Sorted by
Tagged with
0
votes
1answer
61 views

Would this argument support logicism?

Notice the following theory written in multi-sorted first order logic with equality and membership, with axioms of: Comprehension:$\small k=1,2,..,\omega, \omega+1,..$ $\forall x^{i_1},...,x^{i_n} \...
1
vote
1answer
45 views

Expressing binary quantifiers like 'most' and 'finitely many' in second-order logic

I'm revising for a logic exam and in one of the past papers they have a question about the formalisation of quantifiers in first and second-order logic. [In the question, the notation $\phi^{M,g,\...
1
vote
1answer
34 views

How to express ''there exists a subset $X$ of $\Delta$ which is such that at least $50$ percent of $X$ satisfy a property''

In first-order logic, we can use counting quantifier to express ''there exists at least k elements that satisfy a property '', i.e., $\exists_{\geq k} x\colon\varphi(x)$ where $k$ is a integer. For ...
2
votes
0answers
27 views

When can and when cannot a second-/higher-order formula be written as (a countable family of) first-order formulas?

Clearly, not all second-/higher-order formulas can be written as a family of first order formula's. Otherwise we could write the induction axiom for arithmetic as a set of first order formula's and ...
0
votes
0answers
13 views

Theory to Signature Mapping?

So let’s say that I have a theory T with a signature Σ. I want to make another signature Σ’. The logic behind Σ is one/non-sorted, while the logic Σ’ I want to be many-sorted. Is there any means of “...
0
votes
1answer
19 views

What can we do with nonenumerable sets of formulas (e.g. formulas of Higher order Logic)?

It is well known textbook fact, that the set of (grammatically correct) sentences/formulas of higher order logic (even of the second order logic) are not enumerable. My question is - what can we do ...
1
vote
2answers
23 views

Faster Higher-Order Derivatives

so I'm taking a calc class and I got a question to calculate a derivative similar to this one: $\ln((x+1)^4(x+2)^7(x+8)^4)$. I used chain rule and power rule to find that the answer was: $\frac{15x^2+...
2
votes
0answers
68 views

Existence of first-order and higher-order bayesian probability

As normal Bayesian probability could be thought of as zeroth-order or propositional logic where the truth values are real numbers between 0 and 1 inclusive, do there exist Bayesian probability ...
2
votes
3answers
78 views

Using a proof by contradiction with unprovable statement

In a standard proof by contradiction of the statement p => q “p implies q”, we can suppose the statement is false. If we then derive an absurdity then the statement is shown to not be false, hence it ...
0
votes
0answers
33 views

Sequent calculus for classical higher order predicate logic - why not?

I read that there is sequent calculus for second order substructural predicate logic https://link.springer.com/chapter/10.1007/978-3-319-08587-6_5 and sequent calculus for second order (what it means?)...
-1
votes
1answer
58 views

Strategies for translating statements into formal logic language

I've seen many posts asking for help translating a specific statement (posed in natural language) into a formal logic language, and the answers are typically straightforward translations without much ...
1
vote
0answers
39 views

Do non-monotonicity / higher-order / probabilistics / modalities / connectives exhaust all possible features of logical reasoning?

I am searching for all the possible features of reasoning (all of them can be expressed in logic), so far I have found the following features: non-monotonicity, defeasible reasoning (expressed by ...
3
votes
3answers
645 views

Exists infinitely many as a numerical-quantifier

On notation, at first I just write $\exists^{!\infty}$, later I changed to $\exists^\infty$, which one should I use $?$ And I'm thinking what does this really mean in first-order-logic$\dots$ My ...
1
vote
0answers
60 views

Terminal object in a Cartesian Closed Category

Pierce's Basic Category Theory for Computer Scientists writes: 1.10.2 Definition A Cartesian Closed Category (CCC) is a category with a terminal object, binary products and exponentiation. I ...
2
votes
0answers
64 views

An equation involving multisets

For multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, where $...
2
votes
0answers
115 views

ZFC plus HOL-Standardness

I was wondering what happens if we extend ZFC by the assumption that $U$ is a model of ZFC that is 'standard' relative to every definable higher-order theory that is categorical. Specifically: Let ...
0
votes
1answer
94 views

Weak second order Logic

I was reading the other day (Chapter 3 Introduction) , that sequential calculus is also called weak second order monadic logic with one successor or WS1S. I understand the difference between ...
0
votes
0answers
39 views

Is this kind of high order logic of individual predicates inconsistent?

Lets permit quantification over predicate symbols in formulas, so the formula formation rules would the same as those of first order logic, but with allowing quantification over predicates, and ...
12
votes
2answers
531 views

Is many sorted logic really a unifying logic?

I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that "[M]ost reasonable logical systems can be naturally translated into many-sorted ...
0
votes
1answer
80 views

Atomic Formulas in Second Order Logic

I'm studying second-order logic and I would like to know if the phrase about atomic formulas in Figure 1 is correct. If addition, I would like to know what means a second-order predicate like $P^n_k$ ...
2
votes
0answers
117 views

Understanding The First Axiom Of Gödel's Ontological Proof

On Wikipedia, the first Axiom of Gödel's ontological proof is $$(P(\phi)\land\square\forall x(\phi(x)\Rightarrow\psi(x)))\Rightarrow P(\psi),$$ I assume there are implicit quantifiers present for $\...
1
vote
2answers
230 views

If Type Theories are all Logics.

So it sounds like Higher Order Logic (HOL) and Type Theory are equivalent. Then there is Intuitionistic Logic and Intuitionistic Type Theory, but I'm not sure of the connection there. I am just ...
1
vote
2answers
248 views

Paradox vs Tautology.

The expression(~p or p )is a Tautology. Consider this statement(p): This statement is false. Now here, Statement p is paradoxical. My question is :- Can we define paradoxes like this as statements ...
2
votes
1answer
91 views

'Logically symmetric' expressions in lambda calculus

A popular idea among philosophers is that facts are built out of fundamental entities in something like the way that sentences are built out of elementary expressions. My question is motivated by a ...
4
votes
1answer
162 views

How do we get the converse of extensionality in Gödel's 1931 system?

Just had a look at a transcript of Gödel's 1931, On formally undecidable propositions of Principia Mathematica here. The original is found for example here. There is a particular axiom schema V on ...
2
votes
0answers
43 views

Finite axiomatizability of theories in infinitary logic?

I know that the use of axiom schema in first-order theories can usually be eliminated by allowing higher-order quantification. So, a theory that isn’t finitely axiomatizable in a first-order language ...
1
vote
1answer
136 views

Having trouble Solving fourth order heat equation.

I am facing trouble solving this higher order heat equation $$\partial_t u +\partial_x^4 u = 0, \space \space \space \space \space \space \space \space \space \space \space -\infty<x<\infty, t&...
1
vote
2answers
455 views

Axioms in Gödel's ontological proof are inconsistent?

So, my problem is with Axiom 5 of the proof, where Gödel considers necessary existence as a property. However, by his own definition, a 'property' applies to objects including those whose necessary ...
1
vote
0answers
115 views

Modal logic formulation

Introduction So, I want to prove that the decisions that any being makes are either predetermined or are chosen at random - basically, disproving libertarianism. I have already formulated it using ...
3
votes
1answer
1k views

Type theory vs higher-order logic

This is a question about terminology, as I am clearly confused on the topic. The Wikipedia page on higher-order logic defines it as follows: Higher-order logic is the union of first-, second-, ...
2
votes
1answer
90 views

Classifying topos for higher order logic

Chapter X of Mac Lane and Moerdijk's Sheaves in Geometry and Logic focuses on Classifying topoi. The basic concept in the early pages is the one of geometric formula, which is by definition a first-...
1
vote
1answer
39 views

A rule in the recursive clauses governing type formation in a higher order logic

My question regards the theory of types, as augmented and formalised by Richard Montague. On page 10 of Gallin's "Intensional and Higher order modal logic" https://www.elsevier.com/books/intensional-...
1
vote
1answer
60 views

Translation of an argument in logical notation.

I have to formulate the following argument into logical notation : All accused are guilty.All who are convicted will hang.Therefore if all who are guilty are convicted then all the accused will hang. ...
4
votes
1answer
294 views

The place of lambda abstraction in internal and Mitchell-Bénabou languages

It appears that most cases of an internal language/logic/type theory of a category have an appropriate notion of implication/function types and a notion of lambda abstraction that makes use of them. ...
1
vote
1answer
144 views

Third order logic: quantifying sets of sets or relations of …?

I'm reading a book that uses first- and second-order logic. The author defines first-order logic normally, but then defines second-order logic as "quantification on relations." Almost everywhere else ...
1
vote
1answer
148 views

Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa?

Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa? If that could be done then we would be able to import Coq axioms and theorems in Isabelle/HOL. Coq has ...
2
votes
1answer
3k views

Can someone please explain the difference between first/second/third order logic, using examples?

I am currently struggling to get my head around how to recognise the difference between first/second/third order logical arguments. I feel that the easiest way for me to understand the difference ...
1
vote
1answer
2k views

What does second order variable mean?

What exactly does second-order variable mean? I know that first order variable (usually denoted by lower case letters like $p,q,r...$) are those which take the value $T$(true) or $F$(false). I see ...
4
votes
1answer
140 views

Is Axiom IV of System P in Godel 1931 really the axiom of reducibility?

System P in Gödel's original paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" contains the following axiom schema: IV. Every formula derived from the schema ...
1
vote
0answers
22 views

Using compactness to show the existence of an artininian ring with arbitrarily long stricly decreasing sequences of ideals

An example of such an ring is the Prufer group. My question is this - is there a way to use some sort of "compactness" theorem, to show that such a ring exists? Here by compactness I mean something ...
5
votes
2answers
720 views

Topos theory and higher-order logic

[Updated in light of some of the comments and answers below] This is a question about the relationship between higher-order logic and topoi. It's well-known that every topos gives a model of higher-...
0
votes
0answers
57 views

Question about a proof of PA$_2$'s categoricity

Here is a proof of the categoricity of second-order Peano arithmetic. I have trouble understanding a part of it. Let $\mathfrak N=(V',\mathbb N,\text P(\mathbb N),\text P(\mathbb N^2),\text P(\mathbb ...
1
vote
1answer
76 views

Lowenheim Number of L(Q)

Systems Between First-Order and Second-Order Logics by S. Shapiro (in Handbook of Philosophical Logic, vol 1, ed 2) gives a definition similar to the following: Let $L(Q)$ denote the logic that ...
0
votes
0answers
142 views

The relationship between logics and algebraic structures and results in logic that correspond to results in Universal Algebra

Propositional logic is intimately related to Boolean algebra, in the sense that both its syntax and semantics can be given an algebraic interpretation. Are there any algebras that stand to second or ...
0
votes
1answer
101 views

Equality notions in logics other than first order logic

Here https://terrytao.wordpress.com/books/analysis-i/ Terence Tao says: However, the axioms provided are the standard axioms for equality in first-order logic, which already suffices for most ...
2
votes
1answer
189 views

Can a variable depend on an existential variable?

I recently read the following article by Terence Tao: https://terrytao.wordpress.com/2007/08/27/printer-friendly-css-and-nonfirstorderizability/#comment-472808 He writes: “Moving on to a more ...
1
vote
1answer
122 views

Conservative extension in higher order logic?

Specifically I am interested in the prerequisites of a valid extension by definition, like in FOL before introducing an n-ary function symbol (e.g. $f$) for the extension to be conservative we have to ...
-1
votes
1answer
43 views

Logical equivalent of $\phi[x/y]$?

In ZFC if $x\in \{y\in z:\phi\}$ I think it is safe to conclude that $x\in z \wedge \phi[y/x]$ but since $\phi[y/x]$ is not part of the language what is the logical equivalent that is part of the ...
1
vote
1answer
79 views

Formulation of axiom of induction?

Tthe axiom of induction has the following second order formulation: $$\forall \phi :\left(\phi(0)\wedge \forall n\in \mathbb{N} :\left( \phi(n)\Rightarrow \phi(n+1)\right)\right)\Rightarrow \forall n\...
0
votes
1answer
189 views

Examples of problems in second order arithmetic that can only be solved in third order arithmetic

So I was reading about Goodstein Sequences: https://en.wikipedia.org/wiki/Goodstein%27s_theorem where it is given as an example of a theorem that is not decidable in PA but decidable in second order ...