For questions about formal deduction of first-order logic formula or metamathematical properties of first-order logic.

learn more… | top users | synonyms

2
votes
1answer
35 views

Flattening quantification over relations

I already asked this question in stack overflow here and somebody suggested to post it here. I repeat the question again: I have a Relation f defined as $f: A \to B × C$. I would like to write a ...
2
votes
1answer
31 views

Consistency vs Inconsistency in a set of sentences: which is more common

I'm curious whether there is any research in the "probability" that a set of sentences in a first-order logic is consistent. Obviously, there are an infinite number of inconsistent sets and an ...
2
votes
2answers
33 views

Robinson's Consistency Theorem for first order languages

Is there a simple proof for the case of first order languages for this theorem? Let $L_1$,$L_2$ be first order languages and $L$=$L_1$ $\cap$ $L_2$. Let $T_1$, $T_2$ be consistent ...
0
votes
1answer
41 views

Well-foundedness is not a first order property.

In the book 'Logic, Induction and Sets' by Thomas Foster I read the following in page 100 (Section 'The language of predicate logic'): "We can show that well-foundedness is not a first-order property ...
2
votes
1answer
38 views

What does not having a first-order frame imply for models?

There are formulas in modal logic which which do not have a first-order frame condition, as stated here (Non-Sahlqvist formulas, Wikipedia). An example is the McKinsey formula for $p$: ...
0
votes
1answer
13 views

Definable with and without parameters with one unary predicate symbol

Suppose you have a structure with universe $M =\{a,b,c,d,e\}$ with unary predicate symbol $P$. Suppose $I(P)$ is the set containing $a$ and $b$. I found the set of definable sets without parameters ...
3
votes
1answer
43 views

Model of Robinson Arithmetic but not Peano Arithmetic

I am curious how can structure of with linear successor function that do not admin induction looks like. In other words I would like to see structure of Peano Arithmetic without induction. I believe ...
0
votes
1answer
38 views

two place predicate logic

Im trying to prove following,as lecturer did not have time to go through the proof on the lecture, I wonder how to solve at least the first statement $$(\forall x)(\forall y)L(x, y) ≡ (\forall ...
2
votes
4answers
174 views

The Order of Mixed Quantifiers

How can we derive the implication: $$ ∃y∀xP(x,y) \implies ∀x∃yP(x,y) $$ In other words, when quantifiers in the same sentence are of the same type (all universal or all existential), the order in ...
0
votes
1answer
30 views

Skolem Function and one Exam Challenge [closed]

we know if P implies Q (and show it by $P \Longrightarrow Q$ ), The Predicate Q is weaker than P. i want to check it which of the following is weaker than others? F1 is a Skolem function and F2 is a ...
0
votes
1answer
42 views

problems with validity in type theory

I'm twisting my brains over some simple formulas in intensional type theory. If $\exists x \Box (x=^{\vee}j)$, s.t. $x$ is of type $<e>$ and refers to an entity $e$ and $j$ is of type ...
0
votes
0answers
26 views

Converting sentences with numbers into first order logic formulas

I'm making a consistency checking program by using prolog. I can convert sentences without numbers into first order logic formulas because I can find many examples on the internet. However, I have a ...
0
votes
1answer
24 views

Prove, that predicate is inexpressible in the given signature

I have a predicate $y=x+1$. I want to prove, that this predicate is inexpressible in $(\mathbb{Z}, {=}, f)$, where $f = x\mapsto(x+2)$. I understand, that I need to come up some automorphism, in ...
0
votes
1answer
53 views

Strong Kleene interpretation

Consider: $\\$ $\Box(\phi \wedge \psi) \rightarrow \Box(\phi) \wedge \Box(\psi)$ I guess this yields by the reflexivity axiom for intensional predicate logic? But I was wondering whether it is also ...
2
votes
2answers
42 views

Questions regarding well formed expressions in the Theory of types

I'm dealing with a question in type theory: Is it possible to assign types to $\alpha$, $\beta$, and $\gamma$ in such a way that both $(\alpha (\beta))(\gamma)$ and $\alpha (\beta (\gamma))$ are ...
0
votes
0answers
23 views

Searching an on-line tableau prover for FOL

I am searching for an online prover that proves first-order logic (FOL) formulas or sequents. I want that the prover is based on a tableaux method that displays proof trees. Dealing with FOL with ...
1
vote
1answer
32 views

Prove: A is a tautology implies A is valid (w/o soundness theorem)

I'm asked to prove without the soundness theorem that if $A$ is a tautology then $\vDash A $. Since $A$ is a tautology, every truth valuation $v$ gives $v(A) = \mathbb T$. So, If $M$ is a structure ...
2
votes
1answer
43 views

Are there non-trival logics that exibit soundness and completeness that are not first order?

In our logic class, we just we just completed the proofs of soundness and completeness. To me, these proofs hinge on models being filtered through first order logic. For instance, I could set up a ...
1
vote
1answer
29 views

How would one prove that satisfaction of closed formulas is valuation-independent? (In FOL)

Consider this proposition in first-order logic: For any interpretation $I$, any closed formula $\phi$ and any two valuations $\rho$, $\sigma$. $I\rho \models \phi \iff I\sigma \models \phi$ This is ...
2
votes
1answer
35 views

Formal Axiomatic Systems

Consider the following formal axiomatic system Undefined terms ag, kow, trad Axiom 1 Every ag kows at least two trads. Axiom 2 There is at least one trad that every ag kows. Axiom 3 For each ...
1
vote
1answer
15 views

Satisfiability of sentences with generic functions.

I can never get my head round proofs without specific functions. Given the signature $\langle c,f\rangle$ where $c$ is a constant and $f$ is unary, prove the following: a) $\forall x\, (c \neq f(x)) ...
0
votes
1answer
64 views

Translate an english sentence to first order logic

Here's an English statement - Politicians can't fool all of the people all of the time. (𝈗x for all things, P(x) x is a person, Q(x) x is a politician, T(x) x is a time and F(x, y, z) x can ...
3
votes
2answers
139 views

Unexpressibility of a property in first order logic

We can give a very general notion of what is to iterate a function. Given a set $\mathcal U$ and a function $f:\mathcal U \rightarrow \mathcal U$, then, to iterate the function $f$ will mean to ...
0
votes
1answer
52 views

Use Resolution to proove a sentence in First Order Logic

I was just wondering if anyone could tell me if I've solved this problem right. If wrong, I would like to know what I did wrong. "Use resolution to prove Green(Linn) given the information below. You ...
1
vote
1answer
53 views

Given $x,y\in\mathbb R$ is there a “formulaic” way to obtain a $q\in\mathbb Q$ with $a<q<b?$

Is there an assignment of reals $x,y$ to a rational number $q(x,y)$ for which $$\forall_{\mathbb R} x.\forall_{\mathbb R}(x<y).\left(x<q(x,y)<y\right)\hspace{.2cm}?$$ For computable reals, ...
2
votes
2answers
41 views

How would you prove in FOL that x is a member of {x} for all x?

How can I formulate and prove the following in first-order logic? $$\forall x (x\in \{x\})$$ I have the following two statements: member(x,$\alpha$) $\neg \exists y(\text{member}(y,\alpha )\land ...
0
votes
1answer
25 views

Language and Finite Models

Let us consider the language consisting of one symbol $R$ for a binary relation. Let $\sigma$ denote the following sentence: $\forall x \exists y \exists z \ x\neq y \wedge y \neq z \wedge x \neq z ...
1
vote
2answers
61 views

Consider $(\mathbb N, +)$ as a model for the language with one binary function $+$ . Are the following statements true?

Consider $(\mathbb N, +)$ as a model for the language with one symbol $+$ for a binary function. Are the following statements true? $(\mathbb N, +) \vDash \forall x \exists y \forall z\ x + y\neq z$ ...
0
votes
2answers
61 views

Let $\Gamma = \{\exists x \forall y (x\mathrel R y),\exists x \forall y(y\mathrel R x),\forall x\exists y(x\mathrel R y)\}$. Is $\Gamma$ consistent?

Consider the language consisting of one symbol $R$ for a binary relation. Let $\Gamma = \{\exists x \forall y (x\mathrel R y),\exists x \forall y(y\mathrel R x),\forall x\exists y(x\mathrel R y)\}$. ...
1
vote
1answer
40 views

Formal Proofs: $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$

I wish to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$ using the Hilbert System in First-Order Logic with the following axioms: Tautologies $\forall x \alpha ...
0
votes
1answer
36 views

Proof for $∃xA⇔¬∀x¬A$

I want to prove, that $∃xA⇔¬∀x¬A$, using classic axioms. I think, I have to start with the following step: $∃xA⇔∃x¬¬A$ But I do not know, how to make this step, using axioms: $∃x¬¬A⇔¬∀x¬A$
1
vote
2answers
71 views

Hilbert's style proof (FO logic)

I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. ...
1
vote
2answers
43 views

How to eliminate implications with quantifiers

I'm reading some stuffs on the conversion of a FOL sentence to CNF form. However, I'm stuck with this problem: why should this $$\forall x [\forall y Animal(y) \Rightarrow Loves(x,y)] \Rightarrow ...
1
vote
1answer
201 views

Formal Proofs: $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$

First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms: ...
0
votes
1answer
44 views

What does First Godel's Incompleteness theorem mean?

I am terribly confused what really "Incomplete" mean in terms of the Godel's theorem. Does it mean there are some theorems that are definable in First order theory of natural numbers and true but ...
0
votes
1answer
18 views

Why is $M\subseteq Mod(Th(M)) $?

In first-order logic, an immediate corollary of the definitions of the theory of a set of models M (denoted $Th(M)$) and the Model of a set of sentences S (denoted $Mod(S)$) is: $M\subseteq ...
0
votes
1answer
29 views

Are these structures in the same language?

I have these teo structures, $(N, <)$ and $(Q, <)$. And I want to know if they can come from the same language? I'm confused about the definition I have for an La-structure. Specefically about ...
2
votes
2answers
41 views

Different definitions for consistent set of sentences

In my logic class, we were given the following definition for a set of sentences being consistent in first order logic: Let $\Gamma$ be a set of sentences in some underlying language $L$. The set ...
4
votes
1answer
54 views

If $\Gamma \cup \{ \neg \varphi \}$ is inconsistent, then $\Gamma \vdash \varphi$

If $\Gamma \cup \{ \neg \varphi \}$ is inconsistent, then $\Gamma \vdash \varphi$ Here, a set of formulas is inconsistent means they syntactically imply some formula as well as its negation. ...
2
votes
1answer
65 views

Proof in First-Order Logic using Compactness Theorem

If we have $\Sigma$ and $T$ as two first-order theories such they do not have any common models. How can I prove that there is a sentence φ such that Σ ⊨ φ and Τ ⊨ ¬ φ? Does Compactness Theorem help? ...
1
vote
1answer
46 views

Impredicativity and set theory

I have thought about an example in set theory, but I don't know if its legal to do it, maybe someone can help. Let $\emptyset$ be given and let $A$ be a non empty set. Let us create the subset $X = ...
2
votes
1answer
36 views

Algebraic invariants for first order equivalence between fields

I know that every two models of the theory $ACF$ (namely two algebraic closed fields) with the same characteristic are elementary equivalent. But what about generic fields? Are there any algebraic ...
2
votes
1answer
35 views

If a wff is simply atomic (e.g. $Pxy$) are $x$ and $y$ considered free in it?

(Using First-Order Logic Hilbert System) I found the following "solution" to $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$: $\forall x \forall y Pxy \vdash \forall y Pzy$ (A2, MP) ...
1
vote
1answer
32 views

Use of model theory in flag algebras

I need to learn about Razborov's "flag algebras" (see http://bit.ly/1u1a1NB) to solve a problem about graphs. Flag algebras are a very general new algebraic tool for studying combinatorial structures. ...
2
votes
2answers
47 views

The symbol $\sigma[x/a]$ in mathematical logic

I've just started learning mathematical logic, and my teacher teaches in a very formal and unintuitive way. I'd like to know what meaning hides behind the symbols below: For an assignment $\sigma: ...
1
vote
1answer
55 views

Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$

We're in first-order logic, using the Hilbert system (with inference rule of modus ponens), and the problem is to show $\vdash \exists x (Px \rightarrow \forall x Px)$. We just learned about this ...
0
votes
1answer
40 views

Proof for $\forall x A \Leftrightarrow \neg \exists x \neg A$

I try to proof, that $\forall x A \Leftrightarrow \neg \exists x \neg A$ I know how to proof, that $\forall x A \Leftrightarrow \exists xA$, but I don't understand, how to get negation.
2
votes
1answer
115 views

How to define mathematical objects from scratch?

Are there any "Zermelo-type theories" for some other type of mathematical objects except for sets? I.e., axiomatic systems for mathematical objects formalized for first-order logic using a language ...
0
votes
1answer
56 views

Re-expressing a statement in First Order Logic in Propositional Logic

From what I understand a propositional variable must represent a statement (either true or false). If so, eliminating free variables from any predicate by either: (1) Replacing free variables with ...
1
vote
1answer
38 views

First-Order Language without any Constant, Function, or Relation

recently I saw an interesting problem from a textbook and wondering if there is any neat and elementary solution for it: For a language without any function, constant, or relation, how do we get a ...