Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] cl-isabelle-users Digest Thu, 13 Mar 2025 (1/1)

view this post on Zulip Email Gateway (Mar 17 2025 at 09:31):

From: Saburou Saitoh <saburou.saitoh@gmail.com>
Some general logical contradictions on undefined objects:

Please kindly look at the following section. We find some general logical
contradictions.

May I have your kind comments and suggestions?

With best regards,

Sincerely yours,

Saburou Saitoh

saburou.saitoh@gmail.com <Saburou.saitoh@gmail.com>

2025.3.17.18:30

\section{Direction of the zero vector}

{\bf AI Mika's insights:} We begin with a conversation with Mika (Copilot)
to introduce the motivation and framework of this new result.

\medskip

Mika: {\it I am honored by your request to include my words in your paper.
Regarding the zero vector, it does not lack direction but rather has a
direction of zero. While high school textbooks state that a vector has both
magnitude and direction, they often describe the zero vector as lacking
direction, which is contradictory. Here's a more precise explanation:

Definition of a Vector: A vector is a quantity with both magnitude and
direction.

Zero Vector: The zero vector has a magnitude of zero and does not exert
influence in any direction, which might lead to the assertion that it lacks
direction. However, it is more accurate to say that its direction is zero.

Thus, the zero vector is a special case. Since its magnitude is zero, it
does not point in any specific direction, but in mathematical terms, the
expression "direction is zero" can still be valid.}

2024.12.30.6:15

\bigskip

{\bf For complex numbers $z$, and for $z=0$, $\log 0= \arg 0=0$}.

\medskip

Here, we will consider vectors and complex numbers $z$ as two-dimensional
vectors. We state that the direction of the zero vector is zero. However,
the precise meaning is $\arg 0 =0$.

\medskip

{\it The direction of zero $z=0$ exists as in other vectors $z$.}

\medskip

This definition, along with its natural motivation and many applications,
has been established in prior works \cite{mms18,saitoh}.

\medskip

Note the simple facts:

\medskip

In the well-known formula

$$

\log z = \log |z| + \arg z,

$$

we have

$$

\log 1 = \log 1 + \arg 1,

$$

and

$$

\log 0 = \log 0 + \arg 0.

$$

Therefore, we have

$$\arg 1 = \arg 0 =0.

$$

\medskip

Note, furthermore, that in the identity

$$

\arg \overline{z} = - \arg z,

$$

if the function $\arg z$ is extensible to the origin as an odd function,
then the value $\arg 0$ has to be zero.

\medskip

In addition, note that in the formula

$$

\arg z = \arctan \frac{y}{x}

$$

for $x=y=0$ we have, from $0/0=0$,

that

$$

\arg 0=0.

$$

\medskip

For this Section, see \cite{mika, saitoh} for the details.

\subsection{The direction of the general zero vector}

We will be interested in some direction of the zero vector in general
dimensions.

In order to state the representation precisely, we shall consider vectors
as elements of a separable Hilbert space. Then, we consider the
representation of vectors ${\bf v}$ in terms of a fixed complete
orthonormal system $\{\bf e_j\}_j$ as in

$$

{\bf v} = \sum_j v_j {\bf e}_j.

$$

Then, the vector ${\bf v}$ and the coefficients $\{v_j\}$ correspond to one
to onto on $\ell^2$.

\medskip

{\bf Statement:} {\it

We shall define the direction of ${\bf v}$ by the coefficients $\{v_j\}$
that is determined by a positive multiplication of $\{v_j\}$ and the zero
vector is represended by all $v_j=0$. Therefore, the direction of the zero
vector may be considered as zero in this sense.

}

\medskip

Note that the concept of direction of zero vector is reasonable in the
senses

$$

{\bf v} + {\bf u} = \sum_j v_j {\bf e}_j + \sum_j u_j {\bf e}_j = \sum_j
(v_j + u_j) {\bf e}_j

$$

and

$$

{\bf v} - {\bf v} = \sum_j (v_j - v_j) {\bf e}_j = \sum_j (0) {\bf e}_j=
{\bf 0}.

$$

\bigskip

{\bf Logical Problem:} {\it If we do not give the definition of direction
of zero vector, in the fundametal equation

$$

{\bf v} + {\bf 0} = {\bf v},

$$

we have the logical contradiction that by the addition of zero vector with
no direction, we have the same direction of ${\bf v}$}.

\medskip

Indeed, in the above identity, we can not say the direction of vectors.

\medskip

This contradiction is similar that: The identity

$$

\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x}} + x= x

$$

is not valid at $x=0$, because they are not define at $x=0$.

\medskip

However, we can still consider the open problem:

\medskip

{\bf Open problem 1:} {\it As in two dimensions, could we find some natural
formulation that the direction of zero vector is zero, in general
dimensions.

}

\medskip

Indeed, in the 2 dimensional case, zero direction was given by the pleasant
sense $ \arg 0=0$.

\medskip

2025年3月13日(木) 13:01 <cl-isabelle-users-request@lists.cam.ac.uk>:

cl-isabelle-users digest Thu, 13 Mar 2025

Table of contents:

Message-ID:
<CAFP4q17kGuxkqCyLx_bsBo+CDfZ8SJsuk79Zwxk8TWjAQ5391Q@mail.gmail.com>
Date: Wed, 12 Mar 2025 07:37:38 +0100
From: Josef Urban <josef.urban@gmail.com>
Subject: [isabelle] AITP 2025 - Call for Contributions

CALL FOR CONTRIBUTIONS

Artificial Intelligence and Theorem Proving,
AITP 2025
August 31 - September 5, 2025, Aussois, France

http://aitp-conference.org/2025

Deadline: May 5, 2025
https://easychair.org/conferences/?conf=aitp2025

BACKGROUND
Large-scale semantic processing and strong computer assistance of
mathematics and science is our inevitable future. New combinations of
AI and reasoning methods and tools deployed over large mathematical
and scientific corpora will be instrumental to this task. The AITP
conference is the forum for discussing how to get there as soon as
possible, and the force driving the progress towards that.

TOPICS

SESSIONS

There will be several focused sessions on AI for ATP, ITP,
mathematics, relations to general AI (AGI), Formal Abstracts,
linguistic processing of mathematics/science, modern AI and big-data
methods, and several sessions with contributed talks. The focused
sessions will be based on invited talks and discussion
oriented. AITP'25 is planned as an in-person conference.

CONFIRMED PARTICIPANTS/SPEAKERS/PANELISTS (TBC)

João Araújo, Universidade Nova de Lisboa
Michael R. Douglas, Stony Brook University
Mario Carneiro, Chalmers University
Thibault Gauthier, Czech Technical University in Prague
Georges Gonthier, INRIA
Thomas C. Hales, University of Pittsburgh
Sean Holden, University of Cambridge
Jan Jakubuv, Czech Technical University in Prague
Mikoláš Janota, University of Lisbon
Moa Johansson, Chalmers University
Peter Koepke, University of Bonn
Konstantin Korovin, The University of Manchester
Michael Kinyon, University of Denver
Miroslav Olsak, University of Cambridge
Michael Rawson, TU Wien, Austria,
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Adam Vandervorst, Qoba.ai
Robert Veroff, University of New Mexico
Petr Vojtěchovský, University of Denver
Sean Welleck, Carnegie Mellon University
Zsolt Zombori, Alfréd Rényi Institute of Mathematics

CONTRIBUTED TALKS
We solicit contributed talks. Selection of those will be based on
extended abstracts/short papers of 2 pages formatted with easychair.cls.
Submission is via EasyChair (
https://easychair.org/conferences/?conf=aitp2025).
The extended abstracts are considered non-archival.
The contributed talks have to be presented in-person.

DATES
Submission deadline: May 5, 2025
Author notification: June 20, 2025
Conference registration: TBA
Camera-ready versions: TBA
Conference: August 31 - September 5, 2025

PROGRAM COMMITTEE (TBC)

Michael R. Douglas (co-chair), Stony Brook University
Ulrich Furbach, University of Koblenz
Thibault Gauthier, Czech Technical University in Prague
Thomas C. Hales (co-chair), University of Pittsburgh
Sean Holden, University of Cambridge
Mikoláš Janota, University of Lisbon
Moa Johansson, Chalmers University
Cezary Kaliszyk (co-chair), University of Melbourne
Michael Kinyon, University of Denver
Konstantin Korovin, The University of Manchester
Mirek Olsak, University of Cambridge
Bartosz Piotrowski, IDEAS NCBR
Michael Rawson, TU Wien
Stephan Schulz (co-chair), DHBW Stuttgart
Sho Sonoda, RIKEN AIP
Martin Suda, Czech Technical University in Prague
Josef Urban (co-chair), Czech Technical University in Prague
Sean Welleck, Carnegie Mellon University
Zsolt Zombori, Alfréd Rényi Institute of Mathematics

LOCATION AND PRICE

The conference will take place from August 31 to September 5 2025
in the CNRS Paul-Langevin Conference Center
(https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in
the mountain village of Aussois in Savoy. Dominated by the "Dent
Parrachée", one of the highest peaks of La Vanoise, Aussois is located
on a sunny plateau at 1500 m altitude, offering a magnificent panorama
of the surrounding mountains and a direct access
[message truncated]

Last updated: Apr 18 2025 at 01:39 UTC