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)
172
questions
0
votes
0
answers
30
views
If a logic first-order one if it allows variables to range over functions?
Perhaps a stupid question but important to me:
I know that a second-order logic allows predicates as variables, such as:
$$\forall P. P(x) \to P(y).$$
But how about functions? For example,
$$f(x) + 1 &...
- 51
0
votes
0
answers
50
views
Interpreting higher-order intuitionistic logic in typed variable-free combinatory logic
Consider the following typed variable-free combinatory logic:
$\iota$ i the type of individuals.
$o$ is the type of propositions.
If $\tau_1, \tau_2$ are types, then $\tau_1 \to \tau_2$ is the type ...
- 159
1
vote
1
answer
47
views
Definition of integers in higher-order logic
There's the classical of natural numbers in higher-order logic (see the introduction of this page for example).
Is there something similar for integers (elements of $\mathbb{Z}$) ? I didn't find this ...
- 11
1
vote
1
answer
135
views
Can you define a countable set containing undefinable elements?
Is it possible to construct a countable set that contains an undefinable set as an element?
Consider a set $X$ to be definable if there exists a parameter-free formula $\varphi$ in the language of ZFC ...
- 6,245
0
votes
0
answers
24
views
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
More specially, given arbitrary Lean proof/theorem, is it possible to express it solely using first-order logic? If so, is it practical, i.e. the generated FOL will not be enormously large?
I have ...
- 211
2
votes
3
answers
106
views
Do Hindley-Milner theories have a Deduction Theorem?
Deduction Theorem: Given $\Gamma \cup \{A\} \vdash B$, we can deduce $\Gamma \vdash A \to B$
HM Counter-Example (?):
Take $A$ to be $\forall f : \alpha \to \alpha, \forall x : \alpha, f(x) = f(f(f(x)))...
- 151
0
votes
0
answers
39
views
what is the reasoning behind $\sqrt{x^2}=\lvert x\rvert$ [duplicate]
My math teacher told us that 'The square root of a positive number is always positive' and then he gave this relation to us $\sqrt{x^2}=\lvert x\rvert$.
I have been previously taught that any positive ...
0
votes
0
answers
42
views
How can higher-order logic be expressed as many-sorted first order logic?
I know that second order logic (or higher order logic generally speaking) can be expressed using many-sorted first order logic. But I am unclear about the specifics.
Say I have predicate variable $\...
0
votes
0
answers
41
views
Axiomizing meets/joins of a lattice directly instead of quantifiers
The usual strategy of axiomizing logic axiomizes quantifiers first and then defines joins and meets in terms of them later. Can you reverse the order of definitions?
I know various logics can be ...
- 1,242
1
vote
0
answers
36
views
Is there any correspondence between higher and lower order logics vs higher and lower level programming languages?
I work as a programmer, and, outside of work, I sometimes dip into mathematical logic. My intuition alerted me to some possible connections between my job and my hobby, and I thought this might be a ...
- 155
1
vote
0
answers
33
views
What Are Some Reasonable Logical Consequences of a Logical Assertion?
First off, my experience is only with some applications of logic (in linguistics and knowledge representation), as opposed to formal logical analysis. But, I'm looking for a formal answer to my ...
- 111
0
votes
0
answers
55
views
what is the order of the logic and the multi-sortedness of the structures required for rigorous math in ...
Might be a not well-posed question but I hope it makes sense and can be clearly answered.
Iwant to know what is the order of the logic required to work with the following areas of mathematics, to ...
- 4,360
6
votes
1
answer
104
views
Comparing "local compactness numbers" of two strong logics
Given a logic $\mathcal{L}$ (together with a fixed encoding of $\mathcal{L}$-sentences by sets), let $\beta_\mathcal{L}$ be the smallest limit ordinal $\beta>\omega$ such that every $\mathcal{L}$-...
- 229k
1
vote
1
answer
117
views
Löwenheim number of the logic $\mathrm{FOL}[L]$ ($(Lx)[\varphi,\psi]$ holds iff $|\{x:\varphi\}| \ge 2^{|\{x:\psi\}|}$)
What is the Löwenheim number of the logic $\mathrm{FOL}[L]$?
Let $L$ be the quantifier with the intended reading a lot more, and the semantics shown at the end of this section. $D_1$ and $D_2$ are ...
- 9,238
2
votes
1
answer
159
views
λP2, the Calculus of Constructions, and quantifying over propositions
In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$&...
- 123
1
vote
1
answer
70
views
A "set" containing objects of diffrent types in higher order logic
In higher order logic, we can model a set as a function whose images lie in the type of propositions. For example, the singleton $\{0\}$ can be modeled as the function $f: <type\ of\ 0> \...
- 11
0
votes
2
answers
126
views
(How) do theories of higher-order arithmetic have non-$\beta$ models?
I was reading this question about $\beta$-models of $\mathsf{NFU}$ and noticed that models theories of higher-order arithmetic can be or not be $\beta$-models. My understanding is that a $\beta$-model ...
- 9,238
0
votes
1
answer
92
views
Annihilator Method. Getting wrong answer
I am doing by this method
Annihilate this function: $(7x^2+5)e^{2x}.$
I am getting the answer $(D^2-2)^5$, but this doesn't annihilate the function.
What am I doing wrong?
0
votes
0
answers
95
views
Gödel's proof: What if all axioms of a formal system are Gödel sentences
By proof, we know that Gödel's first Theorem applies to certain formal/axiomatic system, while the unprovable statement to which Gödel refers, the so-called "Gödel Sentence", is designed to ...
- 3,814
0
votes
1
answer
56
views
Are more classes of structures axiomatizable as you increase the order of the logic?
This is similar to a question I asked before, but slightly different. Is it the case that $n+1$-th order logic can axiomatize more classes of structures than $n$-th order logic? So, for example, are ...
- 16.8k
0
votes
1
answer
55
views
finding the shape of the higher order equations
Is there any way to find the shape of the higher-order equation like this one? I am more interested in making an initial guess about the shape (fast prediction) and then the process to find it. Any ...
- 153
3
votes
1
answer
129
views
Is the existential quantifier commutative in intuitionistic higher order logic?
In higher order logic, one sometimes defines the existential quantifier by
$$(\exists x. \phi(x)) := (\forall \rho.(\forall x.\phi(x)\to\rho)\to\rho).$$
I am having trouble proving that
$$(\exists x.\...
- 2,642
-1
votes
1
answer
98
views
How foundation of mathematics can be based on a first order logic system?
Let's assume that we have an axiomatic system that utilises the second order logic. Can this system be reformulated in terms of first order logic? I guess, it is not the case, since the second order ...
- 523
1
vote
0
answers
132
views
On a definition in a proof
In https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/intensional-logic-and-twosorted-type-theory/00A76E2304DE453C11F6626B712DB662
the following proposition is presented:
...
- 1,413
1
vote
3
answers
128
views
d^2y/dy^2 expressed in t
Given that $$ x = tln(4t) $$
$$
y = t^3 + 4t^2
$$
Find $ \frac{d^2y}{dx^2} $
in terms of t
For this question is it right for me to say
$$
dx/dt = tln(4t)dt=1+ln(4t)
$$
$$
dy/dt = t^3dt+4t^2dt = 3t^2+...
- 45
2
votes
1
answer
144
views
Strongly constructive proofs: Proofs that don't make use of decidability?
I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic:
A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
- 12.1k
1
vote
1
answer
370
views
Is it fair to say that ZFC axioms can not even be stated in FOL?
The separation axiom of ZFC states
Suppose some set $x$ exists, and let $C$ be any condition. Then there exists a set $y$ consisting of all and only the members of $x$ that satisfy $C$.
To translate ...
- 565
0
votes
0
answers
166
views
Higher order arithmetic, hierarchies and proof theoretic ordinals
I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for the arithmetical hierarchy $(\Pi^0_n$, $\Sigma^0_n)$ and the analytical hierarchy $(\Pi^1_n$, $\Sigma^1_n)$ to ...
- 381
2
votes
0
answers
130
views
Can we blend logic and set theory into ONE system?
Why we cannot coin a logical system without this dicotomy of predicate and terms, that is to say a single sorted logic. So we only have term symbols that at the same time act as predicate symbols. So ...
- 4,137
0
votes
1
answer
100
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} \...
- 4,137
1
vote
1
answer
205
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,\...
- 23
1
vote
1
answer
151
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 ...
- 151
2
votes
0
answers
32
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 ...
- 12.1k
0
votes
0
answers
14
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
1
answer
44
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,353
1
vote
2
answers
97
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+...
- 113
2
votes
0
answers
92
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 ...
- 273
2
votes
3
answers
117
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 ...
- 979
0
votes
0
answers
57
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,353
1
vote
1
answer
300
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 ...
- 2,984
1
vote
0
answers
44
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 ...
- 1,353
3
votes
3
answers
1k
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 ...
- 5,178
1
vote
0
answers
104
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 ...
- 605
2
votes
0
answers
72
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 $...
- 509
1
vote
0
answers
165
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 ...
1
vote
1
answer
256
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 first-...
- 121
0
votes
0
answers
43
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 ...
- 4,137
15
votes
2
answers
954
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 ...
- 638
0
votes
1
answer
142
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
0
answers
133
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 $\...
- 2,948