# Questions tagged [first-order-logic]

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

179 questions
Filter by
Sorted by
Tagged with
11k views

### Why is A implies B true if A is false and B is false?

It seems to me that the 'implies' in English language does not mean the same thing as the logical operator 'implies', in a similar way how 'OR' word in most cases means 'Exclusive OR' in our everyday ...
5k views

### Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
3k views

### Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
577 views

### Term rewriting; Compute critical pairs

I have tried to solve the following exercise but I got stuck while trying to find all the critical pairs. I have the following questions: How do I know which critical pair produced a new rule? How ...
2k views

### What is the relation between First Order Logic and First Order Theory?

I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is ...
197 views

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me $P(... 3answers 4k views ### Is resolution complete or only refutation-complete? Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77. There it is mentioned that "the procedure is also complete". I think this ... 1answer 705 views ### Algorithm for deciding alpha-equivalence of terms in languages with bindings I am interested in the alpha equivalence relation in languages with variable bindings, such as: ... 1answer 474 views ### Differences between basic, complex and terminological facts in a Knowledge Base using First-Order Logic I've been reading the excellent book Knowledge Representation and Reasoning by Ronald Brachman and Hector Levesque. In the beginning of Section 3.2 "Vocabulary" of Chapter 3 "Expressing Knowledge" ... 2answers 792 views ### Why is first-order logic (without arithmetic) VALIDITY only recursively enumerable, and not recursive? Papadimitriou's "Computational Complexity" states that VALIDITY, the problem of deciding whether a first-order logic (without arithmetic) formula is valid, is recursively enumerable. This follows from ... 4answers 191 views ### Can I use ellipses in first order logic I ask, because I have to come up with a first-order logic sentence that shows that there are exactly N objects in the universe. What I've been able to come up with is: $$\forall x \; \exists y_1, ... 3answers 7k views ### Can someone clarify this unification algorithm? I've been having trouble understanding a unification algorithm for first order logic, as I don't know what a compound expression is. I googled it, but found nothing relevant. I also don't know what a ... 1answer 195 views ### Characterising (aa)^* in first order logic In my descriptive complexity class, we've been asked to find a formula that characterises the language (aa)^* (over the alphabet \{a\}) with a first order formula over the language \{<, P_a\}.... 0answers 169 views ### On the Turing Completeness of First Order Logic It is well known that in Descriptive Complexity Theory FO is equivalent to AC0. However, this accepts a couple of a theory and a string <T,s> iff the ... 2answers 2k views ### Why do ¬, ∀ and ∃ have the same precedence? I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ... 2answers 224 views ### Undecidable predicate logic is decidable by people? Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at ... 2answers 3k views ### Predicate Logic Notation: What does a “dot” mean? What does a dot (.) mean in predicates? \forall a \in A. \exists d \in D. H(a,d) Especially, how is the above different to \exists d \in D. \forall a \in A. H(a,d) I've never seen this used ... 1answer 73 views ### Why do TPTP Performance plots look like this? CASC is the premier Automated Theorem Prover competition performed annually at the Conference on Automated Deduction (CADE). The 2017 event has finished on the 9th of August this year. During this ... 0answers 134 views ### Characterization of alpha-equivalence in languages with bindings Following up on this post denoting (x \leftrightarrow y) the permutation of x and y and P[x \leftrightarrow y] the term obtained from the term P by permuting x and y (so for example if ... 2answers 279 views ### First-order logic arity defines decidability? I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong) The question ... 2answers 90 views ### Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis? Recently I was reading again this propositions as types paper by Philip Wadler: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf It gives an impression, ... 1answer 225 views ### Solving SAT using tableau calculus I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ... 1answer 144 views ### How logic programming (especially ASP) is related to the reasoning in (first-order) logic? How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ... 2answers 602 views ### How do we translate first order logic's universal quantifier (the \forall) and the existential quantifier (the \exists) to Prolog? I'm trying to convert some English statements to first order logic statements and I'm trying to use Prolog to verify the translations. My question is: how do I convert a first order logic statement (... 1answer 450 views ### What is the difference between superposition and paramodulation? I am currently writing a paper about automated theorem proving in first-order logic. Equality is not uncommon for mathematical problems and almost every theorem prover like VAMPIRE or SPASS has a ... 1answer 104 views ### The equational theory of regular languages has no finite set of axioms for general alphabets According to Redko the equational theory of regular languages with operations +, \cdot, * over a single letter has no finite set of axioms. Why does this imply that it has no finite set of ... 1answer 1k views ### Difference between First Order Logic and Predicate Calculus I see the two used interchangeably. Is one the subset of the other or are they both the same thing? 1answer 187 views ### Does Herbrand's theorem mean any first-order logic formula can be expressed in CNF? Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic. Is this equivalent to saying that Herbrand's theorem ... 1answer 251 views ### Logical characterization of P versus NP problem (and references for least fixed point logic) Wikipedia says the following (and more) about the logical characterization of the P versus NP problem here: Thus, the question "is P a proper subset of NP" can be reformulated as "is existential ... 1answer 473 views ### in refutation (resolution) can we use a clause that have been resolved In resolution if we have a set S composed of three clause C1, C2 and C3 and we want to proof that C4 is derivable from S using refutation: suppose we've resolved C1 and C2 to C5, can we resolve C1 ... 1answer 2k views ### How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things? I'm working on a program which must use inference in first-order logic, and everything is working great except for 1 thing which I don't understand. The book I'm using, "Artificial Intelligence A ... 1answer 49 views ### Should we not reuse constants in tableaux proofs? I am trying to understand the proof of the following using tableaux:$$ \exists x\forall y.r(x,y) \to \forall x \exists y . r(x,y) $$This is how it works out:$$ (1) \space \exists x \forall y .r(x,... 0answers 43 views ### Modern presentation of Ackermann's “Solvable Cases?” Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ... 0answers 142 views ### Decidability over finite graphs of small degree [closed] Suppose$\sigma$is a vocabulary of First Order logic consisting of one binary relation$E$and let$\phi$be a$\sigma$sentence (FO formula with no free variables). Is it decidable whether there is ... 1answer 304 views ### Why ⊢ for affirmative predicates and ⊨ for ¬negations? I read a book which says that in Predicate Calculus, syntactic theorem proving is identical (complete and sound) with semantic entailment and this is very useful because it is easier to prove positive ... 3answers 292 views ### Represent there are infinitely many in FOL How to represent in first order logic the expression: "there are infinitely many" To be honest I'm confused and not even sure whether you can represent them in first order logic. 2answers 222 views ### Why do the sequent calculus NOT left and NOT right rules work? The rules I am considering are$\frac{\neg A, \ \Gamma \implies \Delta}{\Gamma \implies \Delta, \ A} (\neg L)$and$\frac{\Gamma \implies \Delta, \ \neg A}{A, \ \Gamma \implies \Delta} (\neg R)$I am ... 1answer 135 views ### Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic We can express property that graph has vertex cover of size at most k with first order formula:$$\exists x_1 \exists x_2...\exists x_k (\forall y \forall z (E(z,y) \ \rightarrow \ \bigvee_{1 \leq i \... 1answer 130 views ### What is the difference between$x:A$and$x \Xi A$? Given a type hierarchy$(\tau,\sqsubseteq)$and a signature$(VSym, FSym, PSym, \alpha)$, one says that the typing function$\alpha$assigns to each variable symbol$x \in VSym$a non-empty type$A \...
629 views

I am trying to prove using the resolution technique that the following two clauses are contradicting: $\forall_x Shaves(Barber, x) \iff \neg Shaves(x, x)$ $\exists_x Shaves(x, Barber)$ After turing ...
459 views

### How would one prove the pigeonhole principle with a SAT solver?

Suppose I wanted to find a proof of the pigeonhole principle or show that no proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is ...
258 views

### Propositional logic — syntactical completeness

Lets consider propositional logic. We say a proof system for propositional logic is syntactically (negation) complete if for every $\alpha$, either $\alpha$ or $\neg \alpha$ are provable within the ...
59 views

### Basic second-order logic example contains a mistake?

I'm reading the following course on second-order logic, by Péter Mekis : http://phil.elte.hu/mekis/sol.pdf . The course seems excellent, but I'm stuck on one of his first examples for showing the ...
49 views

### How to describe Deterministic Transitive Closure in FOL?

In "Finite Model Theory and Its Applications", page 152, it is said that Deterministic Transitive Closure, on ordered finite structures, captures LOGSPACE. Hence, taking into account that ...
43 views

### Refutation in first order logic

Consider the following statement In FOL, we can reduce entailment checking to satisfiability checking: $S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called ...
378 views

903 views

### Skolemization with multiple arguments — how to unify

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem. My ...