Questions tagged [first-order-logic]

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

Filter by
Sorted by
Tagged with
22
votes
7answers
8k 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 ...
18
votes
4answers
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 ...
12
votes
5answers
2k 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 ...
10
votes
1answer
451 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 ...
8
votes
3answers
1k 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 ...
8
votes
1answer
177 views

Verify correctness of quantifier elimination, using SAT

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(...
7
votes
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 ...
7
votes
1answer
533 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: ...
7
votes
2answers
602 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 ...
7
votes
1answer
434 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" ...
6
votes
4answers
169 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, ...
6
votes
3answers
6k 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 ...
6
votes
1answer
185 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\}$....
6
votes
0answers
154 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 ...
5
votes
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 ...
5
votes
2answers
175 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 ...
5
votes
2answers
2k 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 ...
5
votes
1answer
63 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 ...
5
votes
0answers
131 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 $...
4
votes
2answers
265 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 ...
4
votes
1answer
200 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 ...
4
votes
1answer
113 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 ...
4
votes
1answer
90 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 ...
4
votes
1answer
728 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?
4
votes
1answer
168 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 ...
4
votes
1answer
300 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 ...
4
votes
1answer
1k 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 ...
4
votes
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,...
4
votes
0answers
38 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 ...
4
votes
0answers
140 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 ...
3
votes
1answer
297 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 ...
3
votes
3answers
107 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.
3
votes
2answers
210 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 ...
3
votes
2answers
78 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, ...
3
votes
1answer
117 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 \...
3
votes
1answer
609 views

Resolution of Barber paradox

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 ...
3
votes
1answer
303 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 ...
3
votes
1answer
239 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 ...
3
votes
1answer
45 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 ...
3
votes
1answer
170 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 ...
3
votes
1answer
169 views

Trying to understand interpretation and denotation in FOL

I am going through the book "Knowledge Representation and Reasoning" by Brachman and Levesque. So an interpretation $ F $ is defined as a pair $ \langle D,I \rangle $ mapping from a set of objects $ ...
3
votes
1answer
346 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 ...
3
votes
1answer
24 views

Extension of Tarski's result on the decidability of reals

Due to Tarski's result, it is well-known that the first-order theory of reals $(\mathbb{R},+,\cdot,<,=,0,1)$ is decidable. I am working on a paper where I need an extension of this result. More ...
3
votes
2answers
740 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 ...
3
votes
1answer
69 views

Implementing abduction over first order theories

I am interested in implementing abduction over a full first order theory ie it may be non-Horn. (Aside: Almost all the references I've seen for abduction operate over Horn theories eg "Modeling ...
3
votes
1answer
73 views

Encoding first order formula (or its tree) into binary string?

How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for ...
3
votes
1answer
143 views

Exercise about First-order logic

I try to express the following statements in first order logic: X is a subset of Y. A set can be uniquely characterised by its elements. The power set p(X) contains all subsets of X. A set X is the ...
3
votes
0answers
53 views

A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)

We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
3
votes
0answers
86 views

How to translate lambda calculus into (first-order, modal) logic, is it possible at all?

It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order ...
3
votes
0answers
78 views

In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...