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
60 views

Certain sequents as inference rules

Fix a signature $\sigma.$ Then a coherent formula is a first-order formula built using only $\{\wedge,\vee,\top,\bot,\exists\}.$ See the link for more information. Furthermore, by a "special" ...
2
votes
0answers
161 views

Semantic Proof of Tarski's Undefinability of Arithmetic Truth

A few years ago I took a logic course and I've since lost my notes. I seem to remember a very semantic proof of Tarski's theorem on the undefinability of arithmetic truth, one that didn't use the ...
2
votes
0answers
44 views

Books/papers on model theory in non-monotonic logic

I am working on a project whose object language is in non-monotonic logic. Since the project involves reasoning about the models, I am thinking of translating a non-monotonic problem into a ...
2
votes
0answers
124 views

Isomorphism of finite models

Let $\mathfrak A$ and $\mathfrak B$ are models of finite signature $\sigma$. Prove that $\mathfrak A$ and $\mathfrak B$ are isomorphic, if $\mathfrak A \equiv \mathfrak B$ and $\mathfrak A$ is ...
2
votes
0answers
67 views

Expressing schedule of reinforcement rule using mathematical logic

I am trying to formalize the rules for application of different schedules in a reinforcement learning in special education. Children learn through trials. Each trial is successful if the child ...
2
votes
0answers
70 views

Help understanding Smullyan’s semantics definition for First-Order Logic

Ref.to Raymond Smullyan, First-Order Logic (1968 – Dover reprint). Some background : [pag.44] - individual variables (to be used bound) and individual parameters (to be used free) [pag.47] - ...
2
votes
0answers
140 views

Questions about semantics for First-Order Logic

The basic clause in the semantic definition of satisfaction for quantifiers in f-o logic cab be stated in two alternative forms (for simplicity I assume a formula $A(x)$ : A) take an assignment ...
2
votes
0answers
80 views

Check that constructed recursive function proves that set is recursive.

Let $\forall\exists$-formula be any formula that looks like $\forall x_1...\forall x_m$$\exists y_1...\exists y_n \phi$, where $x_1...x_m, y_1...y_n$ - variables, $m,n \ge 0$ , $\phi$ - unquantified. ...
2
votes
0answers
80 views

Lowering the power of infinite model

I need to prove that for every infinite model $\mathfrak A$ of signature $\sigma$ exists model $\mathfrak B$ with attributes: $\mathfrak A \equiv \mathfrak B$. $\parallel \mathfrak B \parallel = ...
2
votes
0answers
126 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
121 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
120 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
48 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
175 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
173 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
82 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
74 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
93 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
53 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
156 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
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
75 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
163 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
150 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
201 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
207 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
114 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
83 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
126 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
224 views

Can the reduced product construction generate boolean-valued models?

In model theory, the reduced product construction contains a collection of structures or models, a set I that indexes the collection, and a filter U on I. Ultraproducts are a special case of reduced ...
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
262 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
17 views

Determining whether a truth function can be defined in terms of another

Given an $n$-ary truth function $f$ and $m$-ary truth function $g$, is there a way to determine whether $g$ can be defined in terms of $f$? In other words, is there a systematic procedure that can ...
1
vote
0answers
24 views

Unprovable identity over the integers

I was thinking about Tarski's problem, and was wondering what happens if we have a theory $T$ with two sorts $N,Z$ with intended interpretations $\def\nn{\mathbb{N}}$$\def\zz{\mathbb{Z}}$$\nn,\zz$ ...
1
vote
0answers
35 views

Hilbert style proof for $ \left( \left( A\rightarrow \left( A\wedge \neg A\right) \right) \rightarrow \left( A\rightarrow A \right) \right) $

How can I proof that the following formula is a tautology by using Hilbert calculus? $ \left( \left( A\rightarrow \left( A\wedge \neg A\right) \right) \rightarrow \left( A\rightarrow A \right) ...
1
vote
0answers
31 views

What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and ...
1
vote
0answers
33 views

I'm looking for a good book on FOL and set theory.

I finally decided to really learn some axiomatic set theory, at least the basics. I've studied a bit of FOL, but a review would be nice. In short, I'm looking for a book that focuses on $\sf ZFC$ or ...
1
vote
0answers
27 views

Can we prove undefinability theorem first (using techniques that are different from Godel's) and then deduce Incompleteness from it?

I asked a related question about the matter here in philosophy platform where it was suggested to ask a modified version of the question on Math.se My question is, Is there any known way to prove ...
1
vote
0answers
75 views

Is this translation into symbols correct?

Me and my friend came up with a cool game - we take turns in taking some mathematical theorem stated in English and turn it into a symbolic statement. The rules are this: you are only allowed to use ...
1
vote
0answers
36 views

How to denote a variable is an argument to a function.

How would one write "x is an argument to the function f" in set notation. For instance here is a piece of logic I'm trying to write as set notation: For all x where x is an argument to the function ...
1
vote
0answers
37 views

$4$ or more type $2$ implies $3$ or less type $1$

I'm having difficulties with the logic with the last part of the reformulation part of the problem below. Let $x_i$ be the the number of ships of type $i$ to purchase. For $4a:$ (the ...
1
vote
0answers
36 views

Find a number a using strange computer

IN the $\#1$ slot of the computer memory there is number $a$. The computer is able to sum, multiply, divide and subtract from selected slots, writing the result in to the selected slot. It is also ...