Questions about logic and mathematical logic, including model theory, proof theory, computability theory (a.k.a. recursion theory), and non-standard logics. Consider using one of the following tags: (model-theory), (set-theory), (computability), (proof-theory) if they fit the question.

learn more… | top users | synonyms (1)

1
vote
0answers
32 views

Method for removing redundant values from truth table (homework)

For a boolean formule like a ⋁ b ⋁ c the truth table would look something like: ...
1
vote
0answers
110 views

The set of all philosophers is a camel

In Wilder's book "Introduction to the Foundations of Mathematics," a "proof" for the statement: "The set of all philosophers is a camel" is mentioned in passing as something done by Grelling under the ...
1
vote
0answers
83 views

Help in understanding a “obscure” point in W.Rautenberg's textbook : A Concise Introduction to Mathematical Logic

See Wolfgang Rautenberg, A Concise Introduction to Mathematical Logic, (3rd ed - 2010). I've a problem in "decrypting" the statement and the proof of a theorem [see page 97] : Let $\mathcal L$ be ...
1
vote
0answers
101 views

Range/Image of a Non-Decreasing Total Recursive Function is Recursive

How do I show that the range of a non-decreasing, total-recursive function is recursive? I've made reference to this question, but the method used there is not clear to me. My attempt: Let $f$ be ...
1
vote
0answers
39 views

Set of true statements generated by set of axioms with a binary operator

I wondered about this and I am having a hard time formulating it as a question at all, but I hope I can express something if my wondering here. Assume we have a set $V = \{\mathbb N, +, =, X ,(,)\}$. ...
1
vote
0answers
42 views

Axiomatic system valid, effective but not complete.

Let A be the axiomatic system whose only axiom is the sentence n $\approx$ n and deduction rules $\varphi \rightarrow [\varphi \vee \psi ], \psi \rightarrow [\varphi \vee \psi ], (\varphi, \psi) ...
1
vote
0answers
25 views

Basic questions about descriptive complexity

I'm trying to learn descriptive complexity, and I'm having trouble on a basic level wrapping my head around what it means for a logical formula to define a computational language. I've tried and ...
1
vote
0answers
46 views

Poisson process: Has my book used a necessary condition, when it should have used a sufficient condition?

My book says that if we know that if we are viewing a poisson process with length $t$, and know that $n$ events happened in that interval, than the time that any of those events happened is uniformly ...
1
vote
0answers
46 views

Possible logical meanings of mathematical operations

I'm wondering if there are logical meanings for the mathematical operations (addition, subtraction, multiplication, and division) , from the perspective of each operands?
1
vote
0answers
30 views

Treating a complex argument as a system of linear equations

I've been experimenting with putting logical arguments into matrices by considering it a system of equations and converting the arguments into boolean algebra notation. For example letting ...
1
vote
0answers
391 views

Can I use Strong Induction to prove graph theory? - Hamilton Path/Tournament Graphs

I am working on the below proof. I am still new to proves so I am wondering if you guys can answer the following questions: 1) Did I use the inductive hypothesis correctly here? (By the inductive ...
1
vote
0answers
58 views

Three valued logical problem simplification (or not?)

I have a mathematical/programming question. I have a big datafile (.mat-file) which contains sort of boolean data: it is a matrix of doubles that express the following data: x1 = 1, x2 = 0, x3 = 0, ...
1
vote
0answers
460 views

Validity of three syllogisms with venn diagram

me and my study group are struggling with a "how to proof syllogism conclusions" approach. We got three syllogisms which look like the following: We know for a fact that syllogism #1 and #3 are ...
1
vote
0answers
67 views

Replacement of sentence symbols in a well-formed formula

Suppose $\theta$ is a tautology and $A,B$ are sentence symbols occurring in $\theta$ and $\psi$ is a well formed formula obtained by replacing $B$ with $A.$ Is $\psi$ is a tautology? My proof: We ...
1
vote
0answers
53 views

Use equational proofs to solve the problem

Use equational proof to solve the problem. $ \vdash A \lor (B \rightarrow A) \equiv B \rightarrow A $ These are the axioms and theorems.
1
vote
0answers
75 views

Questions about technical aspects of Gödel's proof of his Completeness Theorem

I'm trying to refresh my knowledge about mathematical logic and I'm still unsatisfied with my insight of Gödel's Completeness Theorem. I have read Gödel's original paper (1930 - reprinted into J.van ...
1
vote
0answers
76 views

Multiple uniqueness cases in first order logic

I'm having some trouble representing the following situation: There are three persons of unique names: Lars, Kirk and James. Each person drinks a unique beverage: beer, vodka and whiskey. Each person ...
1
vote
0answers
54 views

What is the proof-theoretic strength of the predicative second-order theory of real numbers?

The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula ...
1
vote
0answers
68 views

Are there intensional classes independent of the set universe?

The hereditarily finite sets can be regarded as purely extensional sets. Furthermore, they are quite independent of the underlying set universe (at least if we look at them from an extensional point ...
1
vote
0answers
103 views

cut elimination for infinitary logic

Takeuti (1987, 223) derives a cut-elimination theorem for infinitary logic from the soundness-and-completeness theorems. However, is there a way to adapt the original Gentzen-style proof? The ...
1
vote
0answers
92 views

Free variables and universal quantifier in FOL

I've answered to a previous question (@LMZ : Free variables in definitions, asked Dec,15) regarding the common mathematical practice, free variables are implicitly universally quantified. The ...
1
vote
0answers
41 views

Characterizing the field of real numbers in the language of ordered fields

Is there an infinitary formula $\Phi$ (in the language of fields in which countable conjunctions and disjunctions are permitted with finitely many quantifiers $L_{\omega_1,\omega}$) which ...
1
vote
0answers
75 views

Cut-off Subtraction in Coq

I am new to the world of computer assistant proof programs in general, and Coq in particular. As a result, I have sought to prove some elementary results about integers as a way to … At the moment, I ...
1
vote
0answers
35 views

Finding DNF for the given problem (Logic)

I'm struggling to find DNF for the given problem: Whats bugging me, is the last line - I'm seemingly unable to get rid of disjunctions in the first 2nd level parenthesis. Any ideas on what am i ...
1
vote
0answers
34 views

Test axiom in PDL

Wikipedia says the axiom for test in PDL is $$ \langle \psi ? \rangle \phi \leftrightarrow \psi \wedge \phi, $$ but why is this right? (i.e. what does it say?) And what is the corresponding relation ...
1
vote
0answers
74 views

Question about models theory

Which of the models M_1,M_2,M_3 in a picture is atomic? Which is saturated? For the two models that are not saturated, find 1-types which are omitted. For the two models that are not atomic, find ...
1
vote
0answers
60 views

Software tools or libraries for dealing with temporal reasoning (visualization/representation).

Temporal aspect of data with no doubts is an important characteristic for many software systems. I'm interested if there are any tools/frameworks for dealing with temporal data for reasoning on it. I ...
1
vote
0answers
74 views

Induction in the caculus of terms - Mathematical Logic

I'm studying logic from the Ebbinghaus's book "Mathematical Logic" and when I tried to solve some of the exercises doubt rises. Given a calculus C consisting of the following rules: ...
1
vote
0answers
78 views

Are there impossible boolean constructions?

I was reading about logic and I remember, for example: That with the binary $\mathtt{NAND}$ connector can be used to assemble all the other binary connectors - I already know that there are primitive ...
1
vote
0answers
116 views

Peano system vs natural numbers

What exactly is the difference between natural numbers and an arbitrary peano system? In particular there is a proof in my book for recursion on natural numbers, as well as an erroneous proof of ...
1
vote
0answers
77 views

Is this an 'only if' sentence, or a 'if' sentence?

The sentence is: Bertha eats only regularly if Anna does. The only abbreviations are: A: Anna eats regularly B: Bertha eats regularly Is this an 'only if' sentence or a 'if, then' sentence. Is it ...
1
vote
0answers
59 views

Fragments of first-order logic and the functions that preserve them - reference request.

Is there a good resource for learning about different fragments of first-order logic? At this point, I'm mainly just interested in the basic facts, nothing too deep, but preferably presented in a ...
1
vote
0answers
16 views

Can we say that CSL has the same expressive power of PCTL?

In other words, a part from the fact that continuous stochastic logic (CSL) deals with continuous time models whereas probabilistic computation time logic (PCTL) deals with discrete time models, is ...
1
vote
0answers
104 views

Maximally Consistent Set (Proof by Contradiction)

Yesterday, I asked about feedback for a proof of the following theorem For all $\phi$, $\phi \in \Gamma^{*}$ if and only if $\Gamma^{*} \vdash \phi$. My main concern was the first part $(\to)$, which ...
1
vote
0answers
115 views

Question on Model completeness in FOL

Claim: Suppose T is model complete and has a model embeddable in every model of T. Show T is complete. This is in Sacks' book Saturated Model theory, problem 8.4. Is the following proof correct? ...
1
vote
0answers
95 views

Pair of literal unifiable? Howto, rules?

Are these pairs of literals unifiable? How do I determine if they are? What are the rules to go? $p_1([[X,Y]\mid [X\mid Y]],[Y\mid Y])$ $p_1([A\mid B],A)$ If I had to guess my answer would be both ...
1
vote
0answers
51 views

A diophantine definition of the Kleene star

Let $f(x \, | \, y_1, \dots, y_n)$ be a Diophantine polynomial that generates the Diophantine set $F$. By Matiyasevich, the set $F^*$ (Kleene star of $F$) is also Diophantine. My question: how can ...
1
vote
0answers
98 views

How to turn a topological space into a semi-decidable logic?

In two interesting posts(here and here),it is mentioned that "there is a close connection between semi-decidable logics and topological spaces" Michael O’Connor wrote: In fact, given a ...
1
vote
0answers
106 views

Is this first order version of the Collatz conjecture decidable in peano arithmetic?

Let $\phi(x)$ be a first order formula in the language of arithmetic with one free variable $x$. Consider the sentence $\psi_\phi$, defined as: $$\phi(0)\wedge \phi(1) \wedge (\forall x \phi(x) \to ...
1
vote
0answers
34 views

How would Horn resolution work if we had shared variables?

The usual Horn resultion is based on clauses of the following form. We find Horn clauses and Horn goals that read in its full form: ...
1
vote
0answers
91 views

Tarski's axiom implies a proper class of inaccessible cardinals

I'm trying to prove this theorem, but is it even true? A Tarski's class is a set $T$ such that: For each $y\in T$, ${\cal P}(y)\subseteq T$ and ${\cal P}(y)\in T$, and for each $A\subseteq T$ such ...
1
vote
0answers
97 views

Use of first-order logic to formalize scheduling problem

During my placement I have to use SAT/SMT solvers to formalize and solve scheduling problems, but I keep on making mistakes in my assertions so if anyone could help me a little it would be a great ...
1
vote
0answers
69 views

Halting problem some properties

I am referring a little bit to my previous question on http://math.stackexchange.com/questions/392843/existence-universal-goto-programm-turing-machine#= Let $f(n)$ be the output of the universal ...
1
vote
0answers
74 views

An extension of Löb's theorem

This question is an extension question of previous one. link: Löb's theorem and provability Now, there is three sentences, P, Q and R. sort-of-says, they are like following. P: P, Q ...
1
vote
0answers
125 views

How should I prove $\Box (\Box p \rightarrow q) \vee \Box (\Box q \rightarrow \Box p)$ using KT45.

How am I supposed to prove the same using natural deduction? I started my proof with a LEM $$\Box (\Box p \rightarrow \Box q) \vee \neg \Box (\Box p \rightarrow \Box q)$$ I split the LEM via $\vee$ ...
1
vote
0answers
81 views

proof checking machine vs. provability checking machine

Let M be a proof-checking Turing machine which takes two inputs, A and B. : M(A,B) = 0 if A codes a valid proof of the sentence coded by B in ZFC. M(A,B) = 1 if A does not code a valid proof of the ...
1
vote
0answers
74 views

Kolmogorov complexity and type of string

My question about well-known theorems: Theorem: Kolmogorov complexity is not a computable function. And, related, Chaitin's incompleteness theorem. ...
1
vote
0answers
97 views

Define infinite path with a finite relation in a graph with Least Fixed Point logic

Least Fixed Point(LFP) logic (p. 37ff) is an extension of first order logic which enables the usage of the least fixed point of FO-definable operators. For example consider a graph $G=(V,E)$ and ...
1
vote
0answers
249 views

Inverse function in multi-valued logic through the Webb function

Let Webb function in multi-valued logic as $Webb(x, y) = W(x, y) = Inc(Max(x, y))$. There is a theorem about any function in any multi-valued logic can be represented through the Webb function. Then ...
1
vote
0answers
75 views

LTL Proofs (next A <-> A atnext True)

I don't know if this is the correct place for this, but I was reading this: and I don't fully understand how they are forming these proofs. For example, I was trying to follow Proof of (Tb5) ...