Thinking about what an experiment on the foundation of mathematics be like
Besides codes to check consistency of some user inputted model, can we go one step higher and have codes that allow users to specify elements of a foundation and then run proof checks on it...?
0. Begin by specifying a formal language which contains all the symbols we are going to use to describe and construct the objects 1. Next, we specify a logic system which provide us the inference rules and syntax 1a. But first, some primitive notions need to be defined: 1b. Propositions P: These are sentence of the formal language which has a fixed truth value 1c. Truth values V: Every proposition is either False (F), True (T) or Null (O)
1d. Conditional propositions P(): These are sentences which its truth value depends on the object specified in the arguement
Let $G = \{z \in \Bbb C \,|\, z^n = 1 \text{ for some} n \in Z^+\}$. How to show that for any fixed integer $k > 1$ the map from $G$ to itself defined by $z\to z^k$ is a surjective ?
@TobiasKildetoft So, suppose $x\in G$, ie $x^n=1$ for some natural no $n$, and take $\sqrt[k]{x}$, then since $x^{nk}=1$, so $\sqrt[k]{x}\in G$ and $\sqrt[k]{x}\to x$ thus it is surjective.
One level higher than nonassociativity: Deductive system based on equations:
Consider the following:
a+b=cd
Whenever using the algebraic structure you end up with th above equation, then the following can be done:
(a+b=cd)=>(a+b+k=cd)
Note how unlike a usual rewriting system, it is unidirectional. One can imagine in such systems the notion of putting brackets to an expression extends to the whole equation
The result is that if certain derivation is reached, then the possible derivation in the next step is restricted to certain types of manipulations, thus the whole system form a graph made of implications
The system is deductive since the manipulations that are allowed form a fixed set of inference rules
But nothing stopped us from generalising it such that even the rules themselves can be changed depending the sequence of rewriting thus giving a highly abstract notion of path dependence making it a lot more expressive than n category theory
Let $G$ be a finite group which possesses an automorphism $\sigma$ such that $\sigma(g) = g$ if and only if $g = 1$. If $\sigma^2$ is the identity map from $G$ to $G$, prove that $G$ is abelian (such an automorphism a is called fixed point free of order 2).
@TobiasKildetoft Intuitively, I just subtract the degree of the divisor from that of the dividend, and I get the degree of the remainder, what would be the rigorous proof of this?
Dividing $f(z)$ by $z-i$, we obtain the remainder $i$ and dividing it by $z+i$ we obtain the remainder $1+i$, then the remainder upon the division of $f(z)$ by $z^2+1$ is @TobiasKildetoft?
@abcd division algorithm: let $P$ and $D$ be polynomials. Then, there is unique polynomials $Q$ and $R$ such that: 1. $P=DQ+R$, and 2. $\deg R < \deg D$
0. Begin by specifying an alphabet $\mathcal{A}$. This give us the symbols to be used
1. Next, define a formal grammar $\mathcal{G}$ which provide the rules in producing new strings and how they are concatenated, truncated etc.
2. Together, these form the formal language $\mathcal{L}$ where all the details of the foundation $\mathfrak{F}$ is writtened and expressed
3. Next specify a logic $L$ with its inference rules to provide the syntax of reasoning in $\mathfrak{F}$
But before we begin, we need to define a couple of primitive notions:
3a. Truth values: These can be True (T), False (F) or Null (O)
3b. Expression: A string or sentence constructed using $\mathcal{L}$ such that it is well formed (satisfy the syntax given by $\mathcal{L}$). They don't necessary have a truth value.
3c. Proposition P: An expression that has a fixed truth value. Can be though as a 0th argument predicate.
In referring to "the surjection" $\mathcal{O}_K/\mathfrak{a}_1 \to \mathcal{O}_K/\mathfrak{a}_2$ with $\mathfrak{a}_1$ and $\mathfrak{a}_2$ ideals of $\mathcal{O}_K$ is it meant that a coset $k + \mathfrak{a}_1$ is mapped to $(k + \mathfrak{a}_1) + \mathfrak{a}_2$?
If $f_n : X \to \Bbb{R}$ is uniformly continuous for every $n$, where $X$ is a metric space, is $\inf \{f_n \mid n \in \Bbb{N} \}$ uniformly continuous?
@Semiclassical Could you also tell me how does symmetry about the line $x=y$ work? I just know how to test it... by replacing xs by ys and ys by xs and if we get the same equation, the graph is symmetric about $x=y$
As discussed in another room, guys, this is a very veryvery strange limit question that you might be interested to have a look at it, cause it has pontentially unbounded number of terms in it, thus even if the limit for each term exists, the formula $\lim_{n\to a} (f+g) = \lim_{n \to a} f + \lim_{b\to a} g$ may not be valid
@Tanuj Recall that if $f : [a, b] \to \Bbb R$ is a (continuous) function then $$\lim_{n \to \infty} \frac{b - a}{n} \sum_{k = 1}^n f\left (a + \frac{k}{n}(b - a)\right) = \int_a^b f(x) dx$$
@Semiclassical I wanted to understand it in the reflection sense...why does this way work: swap x and y , you get the same equation \implies your equation is symmetric about x=y
We consider in $\mathbb{R}^2$ the basis $B=\{ (2,1), (5,3)\}$ and $C=\{ (1,1), (2,3)\}$ and the mapping $f: \mathbb{R}^2 \to \mathbb{R}^2$ such that $f(x,y)=(x+y,-2x+y)$. Let the matrix $Cf_B=\begin{pmatrix}
\alpha_{11} & \alpha_{12}\\
\alpha_{21} & \alpha_{22}
\end{pmatrix}$. I want to compute ...
It is to model what is represented by the image. For squares, it's easy just take a matrix. Almost every square has 4 neighboring squares, for a hexagonal network it would take 6 neighboors for each box.
Let $f$ be an arbitrary complex function on $\Bbb{R}$, and define $\varphi(x,\delta) = \sup \{|f(s)-f(t)| : s,t \in (x-\delta, x+ \delta) \}$ and $\varphi (x) = \inf \{\varphi(x,\delta) : \delta > 0 \}$. Prove that $\varphi$ is upper semicontinuous, that $f$ is continuous at a point if and onl...
@Semiclassical It is enough for sure. You're asking when n^2 - 7 is a perfect square. That forces n^2 - 7 to be (n-k)^2 for some k. If n > k, (n-k)^2 is less or equal to (n-1)^2, which is why you study the gap n^2 - (n-1)^2.
You need to think about the various cases which I can't be bothered to do right now