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)

Filter by
Sorted by
Tagged with
0 votes
0 answers
26 views

Is there a Turing degree/number of unknowns combination beyond which Diophantine equations are independent of PA?

Is there a certain limit in terms of Turing degree and # of unknowns beyond which Diophantine equations (for positive integer solutions) are independent of PA? Specifically, is it meaningful to talk ...
user avatar
1 vote
0 answers
35 views

Is Kleene's realizability recursive?

Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the ...
user avatar
  • 11
1 vote
0 answers
46 views

Why can't we add a self-consistency axiom to an already consistent system?

Gödel's incompleteness tells us no consistent formal system can prove its own consistency. I understand that we can add an axiom to formal system $A$ stating "$A$ is consistent" and get a ...
user avatar
1 vote
0 answers
52 views

Is it coherent to treat the C programming language as a formal system?

In mathematical logic, a formal system is a structure which includes, amongst other things, a set of axioms, and which is able to determine the truth or falsehood of statements with respect to those ...
user avatar
0 votes
1 answer
32 views

Definition of Locus in Synthetic Geometry?

How is "locus" defined in Euclidean geometry? I know that locus is defined as a set of all points satisfying a certain condition. But how do we define "locus" within an axiomatic ...
user avatar
2 votes
1 answer
35 views

How does the finitely axiomatized formalization of predicate logic correspond to natural deduction for predicate logic?

I'm really interested in using Metamath, but Metamath comes with a funky version of predicate logic. Substitution is not allowed in Metamath, so Metamath employs Tarski's system S2 which is "...
user avatar
0 votes
0 answers
56 views

Given a formal system, determines if 4+3 = 7 is consistent

Given the formal system below: Language:$$\left\{ *,\blacksquare ,\blacklozenge \right\}$$ Syntax: $$ <s>::=<star>,"\blacksquare ",<star>,"\blacklozenge ",\ <star> $$ $$ <...
user avatar
  • 1,071
1 vote
0 answers
68 views

Mathematical Formalism/Framework which describes the Internet [closed]

I have searched for about 30 mins for a purely mathematical/logical description of the internet but I haven't found anything I'm looking for so I have decided to invoke the collective wisdom of stack ...
user avatar
0 votes
1 answer
75 views

Representing first order sentences as conceptual graphs

Here are three first order axioms that represents a part of a mereology theory. Reflexivity $\forall x : part(x,x)$ Antisymmetry $\forall x \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$ ...
user avatar
0 votes
2 answers
63 views

Is the decidability of all possible axiomatizations equivalent to decidability?

Introduction This is a weird take on a few different topics in logic, so bear with me. To frame this question, consider that "axiomatization" is to "theory" as "...
user avatar
  • 3,719
0 votes
1 answer
54 views

How do we classify the obvious fact that $A \xrightarrow{gf} C$ can be decomposed into two arrows? Is it just notational?

The following image is of an app I'm working on called "Abstract Spacecraft". It will allow you to make logical rules and also apply them to diagrams at the click of a button, should the ...
user avatar
0 votes
2 answers
61 views

Generalization of nonexpressibility of solutions

Are there any ideas/areas of math that generalize the idea of when a solution to a question can be expressed in some given formal system? Something that (at least in spirit) covers results like No ...
user avatar
  • 65
2 votes
0 answers
50 views

Help with metalogic induction proof involving string parsing

I have a formal language (basically language of first order logic) in which Wffs are defined by following. String $A$ is a Wff if it satisfies one of: $A$ is atomic $A \equiv (\lnot B)$ and $B$ is a ...
user avatar
0 votes
0 answers
77 views

Do we have to resort to intuition at the very root of our thinking?

Formal first order logic is the foundation of ZFC set theory. This gives me the impression that a theoretical system has to be based on a formal logical system, with its own axioms and deduction rules....
user avatar
  • 1,478
0 votes
1 answer
143 views

Why isn't there an app that allows you to enter in all the rules of a given formal system so that the app supports all formal systems of math?

I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on. I'm wondering, why there isn't yet a software app in which you can ...
user avatar
0 votes
1 answer
93 views

Can you give an example of a non-formal system?

A formal system is defined as an abstract structure used for inferring theorems from axioms according to a set of rules (from Wikipedia). Language, logic and mathematics are considered as formal ...
user avatar
5 votes
1 answer
133 views

Essential undecidability of binary string arithmetic

The weak theory of concatenation of binary strings is essentially undecidable.1 Is Presburger arithmetic with two successors (one for each letter) essentially undecidable? Formally, consider the ...
user avatar
  • 5,070
7 votes
0 answers
148 views

Precise statement of the syntactic category of a logic/type theory, in maximum generality?

I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article,...
user avatar
  • 11.9k
2 votes
0 answers
82 views

Simplest set of axioms and inference rules for first-order logic?

I'm interested in finding the "simplest" formulation of first-order logic. To be precise, what formulation of first-order logic has the fewest total axioms (or axiom schemas, henceforth just ...
user avatar
  • 4,878
0 votes
1 answer
49 views

How to write "the set of all walks of a graph" in formal logic notation?

I have this question on the CS stackexchange to figure out how to model "a walk of a graph" in a custom formal language. I think the problem is that there is not just one walk of a graph but ...
user avatar
  • 3,166
1 vote
0 answers
84 views

How do you formalize this reasoning?

There is this simple number theory problem which says "how many 4 digit numbers that are divisible by 3 and whose digits exclude 2, 4, 6 and 9 exist?" the solution is quite intuitive: each ...
user avatar
  • 63
1 vote
1 answer
93 views

Axiom scheme for mathematical induction in formal axiom system for Peano Arithmetic

I'm reading the book "Gödel's incompleteness theorems" by Smullyan. (I found it online here: https://isidore.co/calibre/get/pdf/5823). In Chapter III he explains the Axiom System for Peano ...
user avatar
  • 163
1 vote
1 answer
91 views

What is a precise definition of soundness?

I'm trying to better understand soundness, especially in contrast to semantic consistency. Here is what I've put together so far: Soundness: A theory is sound if all theorems are true under all ...
user avatar
1 vote
0 answers
72 views

Is it possible to create a "hack-proof" system?

Various organizations, such as DARPA, have purported to create virtually "hack-proof" software systems using mathematical techniques such as formal verification. In short, the idea is ...
user avatar
  • 1,309
0 votes
0 answers
32 views

Is there any technical, mathematical or logical, terminology for a set of propositions, all of which cannot be True at the same time.

As the question states, what is the technical term (if any) for a set of propositions which cannot all be true at the same time. That is to say, If there is a set, $A${x1, x2, x3, ... , xn} for which ...
user avatar
0 votes
0 answers
52 views

Is it possible to list all hidden lemmas of a proof?

I'm studying Imre Lakatos' Proofs and Refutations for my master's thesis. Currently I address the concept of hidden lemmas, which I understand to mean unstated assumptions of a mathematical proof, ...
user avatar
  • 9
2 votes
1 answer
45 views

Beta Reduction Constraints

The definition of $β$ reduction is the following : $$(λx.M)N \rightarrow_{β} Μ[x∶=N] $$ So basically we stop treating $x$ as a bound variable and we perform substitution of the now free variable $x$ ...
user avatar
2 votes
1 answer
96 views

Beta Reduction in Lambda Calculus

I came across the definition of beta reduction in Lambda Calculus which is : $$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the $FV(N)$ are still free after the ...
user avatar
0 votes
1 answer
80 views

Godel Escher Bach: Why is a Godel proof-pair representable in TNT?

On page 441, fundamental fact 2 asserts that: The property of forming a proof-pair is testable in BlooP, and consequently, it is represented in TNT by some formula having two free variables. Why is ...
user avatar
  • 1
1 vote
2 answers
90 views

Formal relationship between rules of inference and the material conditional

I am not $100\%$ clear as to what constitutes the difference between a rule of inference and the material conditional, at least in classical logic. I am using the truth-functional definition of the ...
user avatar
  • 1,454
2 votes
0 answers
74 views

Is there a way to study formal systems in general?

I was reading Gödel Escher Bach, and the author explains that mathematics is just an example of something broader: formal systems. So I wonder wether there exists a theory to study formal systems in ...
user avatar
1 vote
0 answers
52 views

Reading Principles of Mathematical Logic by Hilbert

I want to read Principles of Mathematical Logic by Hilbert and Ackermann. However, I don't know if this is an introductory level text. So I was wondering, is there some background one should have ...
user avatar
0 votes
1 answer
74 views

Describing all formal theory theorems problem

I'm having problems understanding how this works so I'll provide detally explained problem but I'd like if someone could explain it somehow simpler or write it out more step by step than what I'll ...
user avatar
0 votes
1 answer
76 views

Is it possible to add computational facilities to otherwise "mathematical" formal systems by adjoining identities to types?

The following thought has been on my mind for years. Think of $\mathbb{N}$ as the type of all well-formed expressions representing natural numbers. And think of $$\tilde{\mathbb{N}} := \frac{\mathbb{N}...
user avatar
  • 65.1k
0 votes
0 answers
33 views

What differences and relation are between proof systems and deductive systems? [duplicate]

https://en.wikipedia.org/wiki/Proof_calculus says A proof system includes the components: Language: The set of formulas admitted by the system, for example, propositional logic or first-order logic. ...
user avatar
  • 43.6k
8 votes
2 answers
283 views

What's up with the Sheffer stroke axiom?

While reading some old paper on the foundations of set theory, I came across a symbol $\mid$ that I eventually determined was the Sheffer stroke, which is a fancy word for NAND. Wikipedia, and also ...
user avatar
5 votes
2 answers
349 views

Implementing sets in $\lambda$-calculus

Both Set theory and $\lambda$-calculus are considered to be valid foundations for mathematics. Since these are both equivalent (in the sense that any structure that can be implemented in set theory ...
user avatar
  • 510
1 vote
1 answer
95 views

Why doesn't this show that first-order Peano arithmetic is consistent?

SOME PRELIMINARIES: Predicate logic is consistent and complete. In other words, (i) for a closed formula $F$ in predicate calculus with equality and functions, $\vdash F$ if and only if $\,\vDash F$ (...
user avatar
  • 1,009
21 votes
2 answers
2k views

What is the definition of a definition?

In mathematical logic or other formal systems, what is the definition of a definition, formally? If "A" is defined as "B", what is the definition of "A" like? Does it ...
user avatar
  • 43.6k
4 votes
1 answer
378 views

Can inconsistent systems be mathematically interesting/useful?

According to the top answer to this question: Doing mathematics we often have an idea of an object that we wish to represent formally, this is a notion. We then write axioms to describe this notion ...
user avatar
0 votes
1 answer
274 views

What are the relations and differences between formal systems, rewriting systems, formal grammars and automata?

I learned from Herre & Schroeder-Heister's "Formal Languages and Systems" that A formal system is based on a formal language $L$, endowing it with a consequence operation $C: 2^L\to 2^...
user avatar
  • 43.6k
3 votes
1 answer
79 views

Is this property of derivation relation equivalent to idempotence?

In Herre & Schroeder-Heister's "Formal Languages and Systems", on p6, A formal system is based on a formal language L, endowing it with a consequence operation C. This operation C can ...
user avatar
  • 43.6k
0 votes
1 answer
37 views

What is compactness for a deductive system?

In Herre & Schroeder-Heister's "Formal Languages and Systems", on p6, It (i.e. a consequential operation) is called a deductive system, if the consequences of a set X can be obtained ...
user avatar
  • 43.6k
1 vote
0 answers
31 views

Is the semantics of a first order logic system defined as part of the first order logic system?

Does a first order logic system consist only of a first order language a first order deductive system? Is a first order logic system nothing more than a formal system? Is the semantics of a first ...
user avatar
  • 43.6k
1 vote
0 answers
94 views

Is linear algebra a formal system?

By a formal system I mean a system for inferring theorems from axioms according to a set of rules. Essentially I wonder, whether a linear algebra could be viewed as some particular set of axioms from ...
user avatar
  • 717
1 vote
1 answer
67 views

Does a formal system that proves everything that is provable exists?

The Church thesis states that "a function is computable iff it is computable by a Turing machine." Similarly, I wonder if there exists some thesis that states that "a mathematical truth ...
user avatar
1 vote
0 answers
73 views

Are Real Numbers a Formal System?

I don't know a lot of mathematics but I have noticed that every branch of Mathematics has the same structure: some axioms (For example in Geometry might be Euclid's Axioms, in Probability might be ...
user avatar
  • 213
1 vote
2 answers
53 views

Question about MU puzzle from GEB

In MU puzzle: https://en.wikipedia.org/wiki/MU_puzzle#The_puzzle, We have "MU" string and 4 rules. Now when compared this to logic the wiki article says "The MI string is akin to a single axiom, and ...
user avatar
  • 11
1 vote
0 answers
63 views

Is there a point at which you can no longer formally define something in math?

I'll admit this is a bit of a vague question, but I'm having trouble actually formulating it. I understand definitional systems can have recursive definitions however this can turn into nonsense ...
user avatar
  • 172
0 votes
1 answer
46 views

How weak can a formal system be that codifies most formal systems?

As I understand it, most if not all formal systems can be codified in $\mathsf{ZFC}$, because this theory is sufficiently strong that it allows us to define strings, manipulate them, and talk about ...
user avatar
  • 24.8k

1
2 3 4 5 6