# Questions tagged [first-order-logic]

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.

229 questions
Filter by
Sorted by
Tagged with
29 views

### confusion due to the difference of "terms" between FOL and SMT-LIB

In first-order logic (FOL), terms evaluate to values other than truth values, i.e., values of terms are neither true nor false. Reference: Chap. 2.1 from The Calculus of Computation By constrast, in ...
18 views

### How to enumerate theories logically equivalent to natural deduction?

Natural deduction seems to generally be structured around the idea of (an/) introduction and elimination rules(s) for each logical symbol. I heard that that was an attempt to capture the way humans ...
42 views

### What is the corresponding lambda-calculus / proof terms of intuitionistic first order logic? (looking for references)

It is an oft-repeated result that lambda calculi correspond to logics. In particular, recall the following (approximate) relationships intuitionistic propositional logic ⇄ simply typed lambda ...
• 143
1 vote
26 views

### Is stable infinity required of theories combined with model-based theory combination?

In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen ...
1 vote
43 views

### Do stably-infinite theories exclude finite sorts?

Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
14 views

### Question about PNF equivalency in sub-models

I'm given this formula: $\forall x(\forall zR(x,z)\rightarrow\exists yR(y,x))$. Now, the statement that this formula is not logically true in every sub-model of a model that makes it logically true, ...
1 vote
133 views

### Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
• 542
72 views

### Extending Fagin's Theorem to the Polynomial Hierarchy

Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP. I was wondering ...
6 views

• 499
1 vote
39 views

### How do I prove relations of two CTL formulas?

If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
• 324
172 views

### how to do incremental construction of the minimal model in logic programming?

I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
• 1,024
139 views

### Is any 2-CNF has 2-DNF representation?

I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
• 103
166 views

### Can you help me in finding an algorithm that finds the first unique number in an array with lowest position?

I have the following problem to solve: Given a non-empty array A consisting of N integers, the task is to find the first unique number in the array. A unique number is defined as a number that occurs ...
115 views

### 'Someone' in first order logic

I have in the lectures a sentence in English, which I have to translate to First Order Logic. Someone who loves all animals loves all humans. Textbook solution: ∀x.(is_human(x) ⇒ is_animal (x)) ⇒ ∀...
• 33
53 views

### Minimum DNF length of a conjuction of equivalences

Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses. I am puzzled on what approach to take -- whether to ...
• 109
1 vote
91 views

### Understanding unprovable halting, model theory, and (in)completeness

I know computability, but not model theory and logic, so this question may be naive or confused in that respect. A blog post of Scott Aaronson mentions a Turing Machine $M^*$ such that the statement P:...
• 4,179
59 views

### How substituituion composition is associative?

I'm not convinced that substitutions are associative, I read the https://en.wikipedia.org/wiki/Substitution_(logic)#First-order_logic and the https://www.youtube.com/watch?v=_cVNeccMF-E My problem is ...
• 243
1 vote
58 views

41 views

### First-order model checking is not fixed parameter tractable on general graphs

I read that the problem of first-order model checking is believed to be not fixed parameter tractable on general graphs. Why is this the case? Would be happy about some reference Thanks in advance!
1 vote
25 views

### Prove that any first-order logics with equality and a relation/functional symbol of arity more than 1 is undecidable

Definition: A formal logic system is decidable – if there is an algorithm that can determine if any given sentence is a theorem (or not). Based on this definition, I am not sure how to move to prove ...
• 515
88 views

### Is there a quantifier more powerful than the other to determine FOL connector?

So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
31 views

### How can I prove KB╞ α?

Is correct to use ~α as rule to prove KB╞ α? Is possible to unify sentence ~V(x,y) v S(x) with V(N,W)? ...
1 vote
35 views

### First-order iteration operator example

I am reading on https://en.wikipedia.org/wiki/FO_(complexity)#Iterating that FO[$t(n)$] consists in first-order logic with an iteration operator that iterates $t(n)$ number of times some quantifier ...
• 499
74 views

### Conjuctive Normal Form

Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if Q and R have different truth-values; or P and R have the same truth-values. Choose all formulas that are in conjunctive ...
152 views

### Resolution algorithm does not seem to generate the empty clause

Let's assume I have the following 3 clauses: $\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$ and I want to see if our KB entails $\neg U$ so I tried to apply ...
• 143
40 views

### Why is “For all the simple things you have done to me, there exists one thing that makes me happy” FALSE? Use nested quantifiers to prove your point

I've done my due dilligence and tried to answer this question using every resource I could get. KhanAcademy, NesoAcademy, and Rosen's Discrete Mathematics book. I still can't wrap my head around it. ...
• 1
94 views

### Uses of of the one-variable fragment of first-order logic aka S5

I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a ...
39 views

### Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
• 113
1 vote
52 views

### Restriction in description logic

$Human ⊓ ¬Female ⊓ (∃married.Doctor) ⊓ (∀hasChild.(Doctor ⊔ Professor))$ Here, $∃married.Doctor$ means if there exists an individual who is married to Bob belongs to $Doctor$ concept. But my ...
69 views

• 109
1 vote
85 views

Prove or Disprove: There is $\boldsymbol{no}$ alphabet $\Sigma$ and closed formula (no free variables) $\varphi$ above $\Sigma$, such that for any Model $M$ it holds that $M\models\varphi\iff\,|D^M|=\... • 109 1 vote 1 answer 42 views ### Validity of formulas in very specific alphabet Let$\Sigma = \{c_1, c_2, R(\cdot,\cdot) \}$be an alphabet in first-order logic without$=$, where$c_1,c_2$are constant variables and$R$is binary relation. Let$\varphi$be a formula without ... • 109 1 vote 1 answer 102 views ### There is an$n^k$prover if and only if$P = NP\$

I am studying computational complexity using Papadimitrious's book: "Computational Complexity". I am trying to solve the final statement of Problem 8.4.9, but I am stuck and would like some ...
93 views

### Tuple relational calculus: existential quantifiers

I have the following question and given answer: Question: List the names of managers who have at least one dependant. Answer: ...
• 27
24 views

### Partitions of star-free languages and questions on the proof of the Splitting Lemma by Diekert/Gastin

I'm currently reading a paper on First-order definable languages by Volker Diekert and Paul Gastin. Im having trouble understanding a part of the proof for lemma 3.2 (splitting lemma). The part I'm ...
• 321