# Questions tagged [formal-systems]

A formal system is broadly defined as any well-defined system of abstract thought based on the model of mathematics. (Def: http://en.m.wikipedia.org/wiki/Formal_system)

192 questions
Filter by
Sorted by
Tagged with
20 views

36 views

### What happens when we introduce a third 'paradox' possibility to the Halting Machine?

Thanks to Turing, we know that it is impossible to construct a machine that can prove for all machines whether they halt or not. This then has mayor implications on many other fields and theorems, ...
19 views

### Intro to Metamathematics Kleene $\S54$ Lemma IId

In this section, Kleene builds a formal system for primitive recursive functions. The beginning of the proof for lemma IId is skipped because it comes for general properties, but I must be missing ...
66 views

### Codification of a formal language in set theory.

Starting with an arbitrary class of sets $\Gamma$, can you generate a free semigroup $\Gamma^*$ over $\Gamma$ with the group operation of concatenation ($\frown$)? The goal here is to codify a formal ...
125 views

### Reducing number of sorts in formal theory

In Kleene ''Introduction to Metamathematics'' 1971 on pp.420 he shows that if we have a formal system which for some formula $M(x)$ can prove the statement $\exists x M(x)$ then one can introduce a ...
143 views

### What is the purpose of Semantics/Model theory in Mathematical Foundations?

First off I know very little model theory so apologies if I say anything very dumb or offensive to logicians/model theorists. Second I should note that a lot of what I am saying here is motivated by ...
33 views

### Adding constants to formal system

I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability. Consider, for example, that in some formal system we prove that if $a,i$ are ...
57 views

### Infimum and Supremum (of sets) - Formal Concept Analysis

I am taking a course of Introduction to Formal Concept Analysis and I have an uncertainty about the definition of supremum (least comum superconcept) and infimum (greatest comum subconcept) of formal ...
91 views

291 views

47 views

### What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
241 views

### What is the purpose of the Axiom of regularity/foundation?

Besides the axioms of extensionality and regularity, all of the axioms of ZFC either postulate the existence of a set or give a method for generating new sets from existing sets. Extensionality then ...
62 views

### Book request - formal logic

Can anyone recommend a good comprehensive introduction to formal logic? I realise the field is enormous. I am particularly interested in books that a) provide historical context, b) cover both first ...
369 views

### Is every true statement about the natural numbers provable in ZFC?

Related questions: Difference between undecidable statements in set-theory and number theory? Is the arithmetic most mathematicans use a modelled within first or a second order logic? Peano's axioms ...
719 views

### Definition of the bound and unbound variable [closed]

What do we mean by bound and unbound variable? I have difficulty to understand their meanings, Could anyone help me with that?
62 views

### A formal language problem

Translated as best I could the problem is stated as follows: Over the set $A=\{\alpha,\beta,\gamma,\delta,\epsilon,\eta\}$ a model $\mathbb{A}$ of language $\mathcal{L}=\{q\}$ ($ar(q)=2$) is defined ...
170 views

### Show that any monotone boolean function can be realize by the following connectives.

Let the following be the set of connectives involving {$\top,\ \bot,\ \land,\ \lor$}. Set $F \leq T$ Show that any monotone Boolean function $f$ can be realize by a wff (well-form formula) using ...
169 views

### Can one-element set be considered equal to its element?

Are there "interesting" (that is non-trivial, for example not containing only one set) set theories with one element set being equal to their element ($\{x\}=x$ for every $x$)? This question arose ...
495 views

### Are there logics without modus ponens?

The question doesn't go beyond the title. And I don't mean logics that merely just don't have it as a primitive rule - I'm interested in logic where you can't actually use it. I've searched around ...
129 views

### The existence of unprovably unprovable statements provable in ZFC [duplicate]

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably ...
107 views

### Does introducing a new type create a different extension, and is it still conservative?

In this comment on Terry Tao's page about his Analysis I textbook, he writes, If one wanted to do things by the book, what one should actually do each time one introduces a new mathematical object, ...
63 views

### Logic -can it possible we derive all theorems in formal system and we can't derive more theorems?

I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic He say theorems of formal system F should satisfy the two laws : 1) The axioms of F are ...
59 views

### How to express induction when we just have finitely many instances, but still proceed inductively over them

Let $Q$ be some finite set with $n = |Q|$. Then suppose I want to show that for every nonempty subset $P \subseteq Q$ some property $A$ holds. One natural way to approach this is using induction, and ...
158 views

### Axiomatic set theory as a first-order logic theory?

This question is about how accurate is it to say that axiomatic set theory is a first-order logic (FOL) theory? The crux of the matter is the nature of the set comprehension symbol $\{\_ \mid \_ \}$. ...
52 views

### Is there a term for this logical property?

Suppose I am working in a standard formal theory such as ZFC or NBG. Consider this statement: "For all well-formed formulas s, ((there exists a proof p s.t. p is a valid proof of s) --> s)" I'm ...
49 views

54 views

### Find Theorems of a Formal Theory

Going through a book on formal logic, I have encountered the following problem. Since I am somewhat new to formal logic, I am confused about how to approach it. A certain formal theory has exactly ...
41 views

### What is the easiest way to show that a type theory is consistent?

I'm working on presenting an extension of MLTT which uses a (from what I can tell) novel conception of type universes which I believe is not equivalent to the standard Russell/Tarski-style approaches. ...