Questions about mathematical logic, including model theory, proof theory, computability theory (a.k.a. recursion theory), and non-standard logics. Questions which merely seek to apply logical or formal reasoning to other areas of mathematics should not use this tag. Consider using one of the ...

learn more… | top users | synonyms (1)

2
votes
0answers
121 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 ...
2
votes
0answers
114 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 ...
2
votes
0answers
119 views

An example of a proof in sequent calculus

I'm reading Gaisi Takeuti, Proof Theory (2nd ed - 1987), and I'm trying with some exercises. See pag.13 : Ex.2.5.2) Prove the following in LK : $(A \supset B) \supset \lnot A \lor B$. In order to ...
2
votes
0answers
90 views

How much arithmetic can Predicative Second-Order EFA do?

As discussed in this MathOverflow question, I'm trying to find what the result would be of applying a Feferman-Scutte-like analysis to the predicativism of Edward Nelson and Charles Parsons, who ...
2
votes
0answers
47 views

Prove that there are no theorems in which there are no occurrences of disjunction

Ref : Peter Andrews, An Introduction to Mathematical Logic and Type Theory To Truth Through Proof (1986). Exercise X1210 : Does $\mathscr{P}$ have any theorems in which there are no occurrences ...
2
votes
0answers
172 views

Non-Constructive Proofs

I have just started to read more about constructivism and its critique towards classical logic. As I was reading, I came across a passage about non-constructive results, that mentioned the following ...
2
votes
0answers
170 views

Information content of universal sentence

What is the information content of a sentence S like 'one has a successor'. To me, it looks like if we assume no a priori knowledge, both S and it's negation will have equal probablity 1/2. This is ...
2
votes
0answers
75 views

Countable Ultrahomogeneous Structures

I've been learning about countable ultrahomogeneous structures, where ultrahomogeneous means every isomorphism of finitely generated substructures extends to an automorphism of the whole structure. ...
2
votes
0answers
59 views

Difference between defining a constant and beginning with it in a structure

For example, let's suppose that I have my structure $\langle\mathbb{R},+\rangle$ and that $\exists!x\forall a\in \mathbb{R}(a+x=x+a=a)$ as an axiom. In this case $0:=x$. But what if I consider the ...
2
votes
0answers
87 views

How strong is ramified predicative second-order arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
2
votes
0answers
73 views

Tricking the Second Incompleteness Theorem

On Wiki, the Second Incompleteness Theorem reads as For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T ...
2
votes
0answers
92 views

Minimal number of variables in a ZFC-undecidable sentence?

Let $\phi$ be a sentence of set theory. In Prenex form, $\phi$ can be written $$ {\bf Q}_1 x_1 {\bf Q}_2 x_2 \ldots {\bf Q}_n x_n \ \ \psi(x_1,x_2, \ldots ,x_n) $$ where each ${\mathbf Q}_i$ is ...
2
votes
0answers
51 views

Algebraization of attribute-value logic

Jürgen Wedekind ("Classical logics for attribute-value languages", can be googled up) has defined an attribute-value logic as a fragment of predicate logic. There are no predicates except for ...
2
votes
0answers
142 views

What kind of logics satisfy the coincidence lemma?

Lets formulate the incidence lemma as follows. We have a possibly infinite set of variables X and the domain of discourse U. Lets define an interpretation of the variables X in the domain U as a ...
2
votes
0answers
45 views

Is this the right solution?

please state whether this is true/false: Let p = true, q = false, r = true $\neg r \implies (p \wedge \neg q) = true$ [correct?] false $\implies$ true that will be true right?
2
votes
0answers
73 views

Functors that have a natural Isomorphism

Find different functors $T, S: Rng \rightarrow Rng$ both identity on objects IE: for each ring $R, T(R)=S(R)=R$, such that there is a natural isomorphism between T and S. I know that a natural ...
2
votes
0answers
76 views

Proof for a finite number of elements

if I want to proof something for a restricted finite number of elements, meaning the following: Imagine that I have a theorem that is somehow similar to the following: For each element in ...
2
votes
0answers
71 views

The Barcan schema in Modal logic

On page 11 of this article by Timothy Williamson http://link.springer.com/article/10.1007/s10670-013-9474-z#page-12 the Barcan schema in first-order modal logic is discussed. Williamson says, ...
2
votes
0answers
159 views

How to show Simp. and Creat. are $\Sigma^0_2$-Hard

Let Simp={$e:W_e$ is simple} and Creat={$e:W_e$ is creative} I'm having troubles showing these sets are $\Sigma^0_2$-Hard, ie that any $\Sigma^0_2$ set can be many-one reduced to them. I've already ...
2
votes
0answers
263 views

First Order logic with vertex covers

Let $G=(V,E)$ be a directed graph. Let $E$ be a binary relation such that $(x,y) \in E$ iff there is an edge from vertex $x$ to vertex $y$. Let the world of first order interpretation be the set of ...
2
votes
0answers
146 views

Confusion in first-order logic inference

I'm having some difficulty with understanding the following paragraphs taken from the Russell & Norvig’s Artificial Intelligence: A Modern Approach, regarding first-order logic inference: The ...
2
votes
0answers
81 views

Proving that an effective procedure is correct

I will start with definitions, theorems, and a few solved exercises which I am taking as theorems now. My actual question will be last, if you want to scroll ahead to see it. Definitions: (1) The ...
2
votes
0answers
94 views

Ordering of multisets in “Paramodulation based theorem proving”

I'm reading this paper: http://www.lsi.upc.edu/~albert/papers/handbook.ps.gz and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A ...
2
votes
0answers
196 views

Sum and product of an ultrafilter

I know the following simple fact is true, but I can't find a good proof: Over the naturals, the only ultrafilter $\mathcal U$ such that $\mathcal U \oplus \mathcal U = \mathcal U \odot \mathcal U$ is ...
2
votes
0answers
200 views

What is a good software package for ( assisted ) theorem proving and documenting?

Background: An issue in my math study is that I haven't found a good way of storing the theorems ( mostly abstract algebra ) I studied and want to (re-)use in proofs. At the moment I use a personal ...
2
votes
0answers
113 views

Lectures of many valued logic

I am looking for a good introduction to this topic... something with lots of examples and models would be nice. I am specially interested by the case where the truth values are open sets in a ...
2
votes
0answers
82 views

Making a Family of Problems into a Category and defining the Morphisms

This question relates to my previous question found here: Defining Category of Problems Let $\left\{\Pi_i \right\}_{i \in I}$ be a family of problems. Let the solution $u_i$ of $\Pi_i$ lie in some ...
2
votes
0answers
99 views

Introductory text about different stratification methods in higher-order logic and set theory

Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
2
votes
0answers
132 views

Can you express a logic system like S5 using only a Gödel number?

Since logic systems are just statements and/or axioms, can we formulate a logic system gödel numbering the system itself so that the system becomes nothing but a gödel number? For instance the modal ...
2
votes
0answers
128 views

Cut-elimination (transfinite induction base step)

I am having problems with the base step in a proof by transfinite induction. Consider a certain language $Z_{\infty}$, a language similar to PA but with an $\omega$-rule and a cut rule among its ...
2
votes
0answers
252 views

Same same but different: Coextensive relations in model and set theory

The definition of a structure in model theory can be summed up like this (for simplicity's sake without individual constants and functions): Def. 1 A structure is a triple of sets $\langle A, ...
1
vote
0answers
20 views

Structural induction proof

I am trying to solve the following problem, please help me to complete the proof: I need to find the relation between the number of comas in a formula $p_c$ of language L = {f,g} and the number $p_f$ ...
1
vote
0answers
37 views

Differenct axiomatizations of set equality

I've seen two definitions (or axioms?) of set equality: $a=b \Leftrightarrow (\forall x : x \in a \Leftrightarrow x \in b)$ $a=b \Leftrightarrow (\forall x : a \in x \Leftrightarrow b \in x)$ That ...
1
vote
0answers
19 views

How can we prove a statement is provable?

Given a concrete mathematical statement, such as BSD conjecture(https://en.wikipedia.org/wiki/Birch_and_Swinnerton-Dyer_conjecture), do we know if it is provable?
1
vote
0answers
15 views

How to solve this equation using semantic equivlence

Hi I am trying to workout the solution to this propositional logic formula using the below semantic equivalence formula but I am stuck. Could someone please help me out. These are the rules ...
1
vote
0answers
48 views

Theories of Arbitrary Morley Rank

Suppose that you have a language $L$. I can show that theories like DLO, or any unstable theory for that matter, has Morley Rank $\infty$. I can also show that $REI_\alpha$ has Morley rank $\infty$, ...
1
vote
0answers
21 views

If $T$ is a set, $P(x)$ denotes x is a hard worker and $D(x)$ denotes that $x$ is a worker, how to translate the following to English sentence?

So $T$ is a set of workers and materials in a tower, $P(x)$ denotes that $x$ is a hard worker and $D(x)$ denotes that $x$ is a worker $\forall x \in T: [D(x) \rightarrow [\exists y \in T: P(y)]]$ ...
1
vote
0answers
34 views

Translate from logical expression to regular expression

I have a type of exercise in which I want to translate a formal logical expression to regular expression. Now my question is, is there a set of rules which I can learn so I will be able to do this ...
1
vote
0answers
37 views

Checking if $p$ tautologically implies $q$

What is the difference between $p\Rightarrow q$ and $p\to q$? Is $p\to q$ a necessary and sufficient condition for checking $p\Rightarrow q$ is a tautology? Are there alternative approaches?
1
vote
0answers
22 views

Question in regards to representing propositons with P/~P

In a standard Frege-System does it break any rules to have 'P' stand for, say "Smith is not president"? Is it mandatory that such a statement be represented by '~P', or can it indeed be represented ...
1
vote
0answers
45 views

Prove or disprove: MSO can be used to express finite models over an empty signature

The question is: There is an MSO sentence ϕ, over the empty signature, such that M⊨ϕ if and only if M has a finite universe? I think it isn't true because I cannot express the idea of a 1-1 function ...
1
vote
0answers
34 views

Soundness of Propositional Logic proof.

Let $$\begin{align} A1&=(p\implies (q\implies p)) \\ A2&=(((p\implies (q \implies r)) \implies ((p\implies q)\implies (p\implies r))) \\ A3&=((\neg p \implies \neg q ) \implies ((\neg p ...
1
vote
0answers
49 views

Logical shenanigan or not: replacing unbounded quantifiers with bounded one

This can't possibly be right, is it? This is 1 basic line of an argument I found in a paper, which is replicated in many other sources, and the same kind of argument is used in other papers, so I am ...
1
vote
0answers
23 views

“Relative unsatisfiability” of SAT instances

There's a natural way to view any SAT instance as a variety: just replace the Boolean algebra $2$ of truth values with the corresponding Boolean ring $\mathbb{Z}/2\mathbb{Z}$. (See my answer to Is ...
1
vote
0answers
43 views

Relations between statements involving universal quantifier, conditional and biconditional

If we consider two predicates: $b(x)$: x is a boy $c(x)$: x is clever Then, there are four statements involving $∀, b(x), c(x), →$ and $↔$ . These are below along with my interpretation of their ...
1
vote
0answers
82 views

Can you define a sensible probability measure on the set of countable transitive models of ZFC?

It is well known that the set of hereditarily countable sets $H(\omega_1)$ —or, if you prefer, $H_{\omega_1}$— has cardinality $2^{\aleph_0}$, and I understand that every countable ...
1
vote
0answers
17 views

Is Grzegorczyk's theory $TC$ interpretable in Robinson Arithmetic $Q$

The question is in the title. It is known that $TC$ interprets Robinson Arithmetic $Q$ (Svejdar proved this), but I am interested in seeing the proof of the other direction. My motivation for the ...
1
vote
0answers
39 views

Unit of Probabilities with uncertainties and contradictions

I want to built a unit of information, somewhat like a qubit, but it should encode besides the real-valued 'value' also the measure of 'uncertainty' (inverse of confidence) and measure of ...
1
vote
0answers
41 views

Optimal object in category? Metric, objective function on category objects. Optimization over category?

Is there notion about optimal object in category (that can be found by some algorithms, or - more importantly - that can be constructed (if unknown) by some algorithms), about metric and objective ...
1
vote
0answers
32 views

iterated unprovability

Hi all the following might be a silly question it is well known that some statements like for example CH are not provable within ZFC (assuming consistency of course) ie. $ZFC\not\vdash CH$. However, ...